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: Oct 03 2023 at 04:02 UTC