Add/redefine (axiomatized) instances for redefined types

[lastland]

Issue by sweirich
Monday Jul 01, 2019 at 15:20 GMT
Originally opened as antalsz/hs-to-coq#136

---

If we redefine a type to axiomatize it:

redefine Axiom M.myType : Type.

It would be good to be able to add axiomatize a default instance for this type. Adding this instance in the midamble is too late --- a generated default instance or partial record selector may depend on it.

[lastland]

Comment by antalsz
Monday Jul 01, 2019 at 16:41 GMT

---

How easy is this to work around?

[lastland]

Comment by sweirich
Monday Jul 01, 2019 at 17:53 GMT

---

This isn't urgent. It turns out it is better to keep the type axiomatizations in a separate module instead of trying to add them to Core.v. That way we can break more module import cycles.