Commit 099ef7a

committed

Erase function lemma (#1053)

* Fix typed erasure calls to _not_ trim inductive masks * Comment WIP app_construct proof * Comment WIP erase_function proof * Prove that functions are preserved by compilation * Show that inhabitants of product types evaluate to functions through the erasure pipeline

1 parent 7039be2 commit 099ef7aCopy full SHA for 099ef7a

1 file changed

+667

-13

lines changed

erasure-plugin/theories
- ErasureCorrectness.v

1 file changed

+667

-13

lines changed

Comments

(0)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Commit 099ef7a

1 file changed

1 file changed

File tree

1 file changed

1 file changed

0 commit comments