gistfile1.txt

Code::

// Env = current environment
// matchExpr = entirety of following block

match (expr) as y in T x_1 x_2 .. x_n return RExpr with
  | ...
  | Ci y_1 ... y_m => D_i
  | ...
end
=====================================



Typing Rule:


Env |- expr : T u_1 ... u_n

repeat {
  Env |- Ci : forall (_: a_1) (_: a_2) ... (_: a_m), T w_1 ... w_n
  Env (y_1 : a_1) (y_2 : a_2) ... (y_m : a_m) |- D_i : RExpr (y / C_i y_1 ... y_m; x_1/w_1, ..., x_n/w_n)
}

--------------------------------------------------------------------------------------------------------------

Env |- matchExpr : RExpr(y/expr, x_1/u_1, x_2/u_2, ..., x_n/u_n)