The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hey,

> 1) first_of_htree =
> 2) fun (A : Set) (n : nat) (v : htree A n) (t : htree A (S n)) =>
> 3) match t in (htree _ n0) return (htree A (pred n0) -> htree A (pred n0)) 
> with
> 4) | hleaf _ => fun v' : htree A (pred 0) => v'
> 5) | hnode p _ t1 _ => fun _ : htree A (pred (S p)) => t1
> 6) end v  (*this v confused me*)
> 7)      : forall (A : Set) (n : nat), htree A n -> htree A (S n) -> htree A 
> n
> ---------------------
> I do not know the exact meaning of "end v" in the sixth line.

The 'match' statement returns a function; this function is then applied
to 'v'.

Edsko