Just some information for those of you relying on MetaCoq:
- we finally have all the cumulative inductive type theory formalized, it does enjoy subject reduction, "weak" principality and does not invalidate elimination principles needed for erasure.
- we didn't find a way yet to extended the formalisation with eta-conversion. As such our first "beta" release will not have it, and I'll remove the "todoeta" axioms that appear here and there.
- the metatheory of pcuic is otherwise admit-free.
- once this cleanup is done I'll release a beta package (working with ocaml 4.10 hopefully).
may I suggest that the beta version(s) be called
Last updated: Feb 09 2023 at 02:02 UTC