CODEWITHSUNDEEP
coqcoq-tactic
g_d
g_d

Reputation: 707

Tactic to partially compute goal in Coq

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

Answers (1)

Vinz
Vinz

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

Related Questions