The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Le 22 oct. 2013 à 11:36, t x 
<txrev319 AT gmail.com>
 a écrit :

> Suppose now, instead of trying to understand "how to use Coq", we are 
> interested in "how to implement a verifier" then is the following 
> pseudocode correct ?
Nope

Let's omit the fact that there may be arguments as you do
> 
> (* let matchExpr = entireity of the following block *)
> match (expr) in y as T x_1 x_2 .. x_n return RExpr with
>   | C1 y1_1 y1_2 ... y1_m1 => D1
>   | C2 y2_1 y2_1 ... y2_m2 => D2
>   ...
>   | Ck yk_1 yk_2 ... yk_mk => Dk
> end
> 
> then, we can say that:
if expr has type T u_1 u_2 .. u_n then matchExpr has type 
RExpr/{x_1=u_1,x_2=u_2 .. x_n=u_n;y=expr}
> 
> if:
>   forall 1 <= i <= k, we have:
if Ci has type forall yi_1 .. yi_mi, T v_1 .. v_n then Di has type 
RExpr/{x_1=v_1,x_2=v_2 .. x_n=v_n;y=Ci yi_1 .. yi_mi}
> 
> -- and this is actually all there is to it, no?
Nope again
fun x_1 … x_n y => RExpr has to be well typed (else Coq would have JMEq_eq !)
> 
> (sorry for beating this zombie horse to death)
Pierre B.