Antal Spector-Zabusky

They can now be `skip`ped, but not `redefine`d

This is a really lovely idea, but I'm not sure how feasible it is. We initially focused on providing a generic Coq AST, but through accretion and gradual change we've...

One possible new structure: 1. An `hs-to-coq` repo containing `hs-to-coq`, along with a couple of examples showing how to use the tool. These examples should be *static* – they're documentation....

We have the following edit in `CoreUtils/edits`: in CoreUtils.eqExpr rewrite forall p, Util.all2 p a1 a2 = NestedRecursionHelpers.all2Map p id id a1 a2 We wouldn't need this at all if...

This also extends to improving the Coq parser, such as by supporting `let 'pair x y := ... in ...`.

And being consistent in where we apply `rewrite`s – for instance, we don't currently rewrite all generated `match`es

@sweirich Well, at a minimum, `translate` is a *much* better name than `unaxiomatize` 🙂 The logic does make sense. The only design question I see is that going from `skip...

So the design structure is: * Module → {Translate, Axiomatize, Skip} * Definition → {Translate, Redefine, Axiomatize, Skip} Per-definition rules take precedence over the by-module rules. We leave `skip method`...

We have `axiomatize definition` working – is that what you mean?

No – mostly because we don't check, although also because we don't have kind signatures that we can fill in.