Stream: Coq users

Topic: How to write statement?

view this post on Zulip 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 .

How to assign functions value to eqs?

view this post on Zulip 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 (
The software foundations course ( (or any other Coq course) should cover those uses :)

Last updated: Sep 23 2023 at 06:01 UTC