zohaze (Nov 01 2022 at 12:12): 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?
James Wood (Nov 01 2022 at 13:42):Please provide the code reproducing your issue.
Last updated: Oct 03 2023 at 04:02 UTC