CharlesAverill/volpic

Haskell Extraction

Opened this issue · 0 comments

Volpic_preamble.v currently assumes OCaml as the extraction language (because I'm lazy). Will eventually need to parametrize this. Ideally, I have a general preamble and a parametrized preamble that I glue together.