% % typeof E A : (Non-elaboration) source typing, without subsumption rule % typeof : exp -> ty -> type. %name typeof _Typeof. % Top typeof/topintro : is-value V -> typeof V topty. % Intersection typeof/sectintro : typeof E A1 -> typeof E A2 -> typeof E (sectty A1 A2). typeof/sectelim1 : typeof E (sectty A1 A2) -> typeof E A1. typeof/sectelim2 : typeof E (sectty A1 A2) -> typeof E A2. % Union (and 'direct') typeof/unintro1 : typeof E A1 -> typeof E (unty A1 A2). typeof/unintro2 : typeof E A2 -> typeof E (unty A1 A2). typeof/direct : {EC : eval-context} fill EC EH -> typeof E' A -> ({x : exp} typeof x A -> typeof (EH x) C) -> typeof (EH E') C. typeof/unelim : {EC : eval-context} fill EC EH -> typeof E' (unty A1 A2) -> ({x1 : exp} typeof x1 A1 -> typeof (EH x1) C) -> ({x2 : exp} typeof x2 A2 -> typeof (EH x2) C) -> typeof (EH E') C. % merge typeof/merge1 : typeof E1 A -> typeof (merge E1 E2) A. typeof/merge2 : typeof E2 A -> typeof (merge E1 E2) A. % Arrow typeof/arrintro : ({x : exp} typeof x Adom -> typeof (Ebody x) Acod) -> typeof (lam ([x] Ebody x)) (arr Adom Acod). typeof/arrelim : typeof E1 (arr Adom Acod) -> typeof E2 Adom -> typeof (app E1 E2) Acod. % Fix typeof/fix : ({u : exp} typeof u A -> typeof (Ebody u) A) -> typeof (fix ([u] Ebody u)) A.