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 .
  end.

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 (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