The Coq mailing list

[t x <txrev319 AT gmail.com>]

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 ?

(* 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:

  * matchExpr has type RExpr/{y=expr}

if:

  forall 1 <= i <= k, we have:

    normalize(RExpr/{y=Ci yi_1 ... yi_mi}) = normalize(Di)

-- and this is actually all there is to it, no?

(sorry for beating this zombie horse to death)