Stream: Coq users

Topic: eq-refl


view this post on Zulip zohaze (Nov 01 2022 at 12:12):

I have data type area. Used notation is A(x,y,z). where x & y:nat & z is element of another data tpe space
I have written eq_refl as
Axiom eq_refl : forall d : area, d == d.
But i want to write it in terms of notation as
A(x,y,_)==A(x,y,_). But it gives error. How i can remove it?

view this post on Zulip James Wood (Nov 01 2022 at 13:42):

Please provide the code reproducing your issue.


Last updated: Jan 29 2023 at 01:02 UTC