Inductive compare : Type := | eq1 (a b: nat) | eq2 (a b: nat) | eq3 (a b: nat). Fixpoint eval (a b : compare) : nat := match a b with |eq1= f1 a1 a2 |eq2= f2 a1 a2 |eq3 = f3 a1 a2 . end.
How to assign functions value to eqs?
Hi zohaze ! Could you be a bit more explicit on what you tried an what did not work ? Were happy to help you out, but here the output of Coq and the examples of the documentation should guide you (https://coq.inria.fr/refman/language/core/variants.html#definition-by-cases-match)
The software foundations course (https://softwarefoundations.cis.upenn.edu/lf-current/index.html) (or any other Coq course) should cover those uses :)
Last updated: Jan 27 2023 at 00:03 UTC