Code

Erase function lemma#1053

Code

Merged

mattam82 merged 5 commits intocoq-8.17MetaCoq/metacoq:coq-8.17from erase-function-lemmaMetaCoq/metacoq:erase-function-lemmaCopy head branch name to clipboardFeb 13, 2024

Commits

Commits on Feb 13, 2024

• Fix typed erasure calls to _not_ trim inductive masks

  mattam82

  committed
  636160c

  Copy full SHA for 636160c

• Comment WIP app_construct proof

  mattam82

  committed
  1a7b017

  Copy full SHA for 1a7b017

• Comment WIP erase_function proof

  mattam82

  committed
  9194b08

  Copy full SHA for 9194b08

• Prove that functions are preserved by compilation

  mattam82

  committed
  64db6e3

  Copy full SHA for 64db6e3

• Show that inhabitants of product types evaluate to functions through the erasure pipeline

  mattam82

  committed
  7046d0d

  Copy full SHA for 7046d0d