The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

2014-04-05 23:13 GMT+03:00 Daniel Schepler 
<dschepler AT gmail.com>:
>   Fixpoint nth_triangle_aux {T : Type} (idx stop : nat) (tr :
> triangle_t T idx) : Vector.t T stop :=
>     match eq_nat_dec idx stop with
>     | left e => match e in (_ = stop') return Vector.t T stop' with
>                 | eq_refl => match tr in (triangle_t _ idx')
>                              return (Vector.t T idx') with
>                              triangle _ v _ => v
>                              end
>                 end
>     | right ne =>
>       match tr in (triangle_t _ n) return (S idx = S n -> Vector.t T stop)
> with
>       triangle n _ tr' => fun eq : S idx = S n =>
>              match eq in (_ = Sn) return (triangle_t T Sn -> Vector.t T 
> stop)
>              with
>              | eq_refl => fun tr' => nth_triangle_aux (S idx) stop tr'
>              end tr'
>       end eq_refl
>     end.

This code has some constructs that I never saw before(match ... in ...
and match ... return ...), I had started proving useful theorems in
proof mode(I implemented a non-trivial language and proved type
soundness of it) but apparently there are a lot to learn on
programming side. I'll start reading CPDT from chapter 6.

Thanks again!

---
Ömer Sinan Ağacan
http://osa1.net