```
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: Jun 20 2024 at 11:02 UTC