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?
Please provide the code reproducing your issue.
Last updated: Jan 29 2023 at 01:02 UTC