The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 13 Apr 2014 06:21:25 +0300,
Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 a écrit :

> Thanks for your answer, it worked! I don't understand how can this
> code work, though. Because pattern matching has different return type
> than the function.

Once your proof script is accepted, simply run "Print <term>." to see
it.


Lemma identity : forall A, A -> A.
Proof.
  intros T.
  intro t.
  exact t.
Defined.

Print identity.
=======================
identity = fun (T : Type) (t : T) => t
     : forall A : Type, A -> A

Argument scopes are [type_scope _]



Thus if you can do a proof script and you do not understand how to
write the term, you can read the Print output to get the idea.

> 
> Also, I tried replacing `v'` with `_` and using `refine` tactic, but I
> didn't get `Vector h' 0 someFreshVar = v'` as hypothesis while filling
> the case with `as v'`. Why I never get this types of equalities in
> pattern matching?
> 
> Thanks again.
> 
> ---
> Ömer Sinan Ağacan
> http://osa1.net