zohaze (Dec 31 2021 at 07:15): zohaze (Dec 31 2021 at 07:15):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?
Clément Blaudeau (Dec 31 2021 at 11:32):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: Sep 23 2023 at 06:01 UTC