gistfile1.txt

Code::
 
(* let matchExpr = entireity of the following block *)
match (expr) as y in 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
=====================================
 
Typing Rules:
 
let type(expr) = T u_1 ... u_n
 
if:
  forall 1 <= i <= k,
    normalize(RExpr/{y=Ci yi_1 ... yi_mi; x_1 = u_1, ..., x_n = u_n}) = normalize(type(Di))
 
then:
  matchExpr has type: RExpr/{y=expr, x_1 = u_1, ..., x_n = u_n}