2

I've been trying to find a good guide/read/set of exercises on Coq Contexts, evars, e* tactics etc.

Ideally I want to build a Coq context with some vars abstracted, which I'll fill in later in the OCaml or Haskell extraction. Is that possible and what's the best place to read about theorem holes and how to fill them up in Coq proofs?

rausted
  • 951
  • 5
  • 21
  • 3
    Generally, Coq won't let you close out a proof or definition without instantiating all the evars that have been created over the course of the proof. It sounds like what you need is probably more like a `Parameter` declaration. – Daniel Schepler Feb 13 '18 at 18:50
  • Awesome Parameters does sound like what I want! Now to figure out how to pass them inside Haskell. – rausted Feb 14 '18 at 03:57

0 Answers0