Reputation: 707
I have goal
quad X Y
, but I don't remember definition of "quad" and I don't want to start searching of its definition.
Is there a tactic that allow me rapidly substitute quad with its definition?
Record quad (X Y:Type):= { x:X; y:Y}.
Or I have to remember and use
refine (@Build_quad _ _).
?
Upvotes: 1
Views: 94
Reputation: 6057
Your slightly mistaken, Build_quad
is not the definition of quad
, it is its constructor. It creates terms of type quad
.
As @ejgallego said, you should use the constructor
tactic in this situation.
Your goal wants you to provide a term of type quad X Y
, and the only way to build such a term from scratch is to use the constructor Build_quad
of type forall X Y: Type, X -> Y -> quad X Y
.
Upvotes: 3