MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
380 stars 82 forks source link

Proof that reordering of constructors is correct #1095

Closed mattam82 closed 3 months ago

mattam82 commented 3 months ago

We show that e.g. Extract Inductive bool => "bool" [ 1 0 ] is semantics preserving, so that we can map to the target language's data representations directly (e.g. ocaml's booleans).