diff options
Diffstat (limited to 'language/l2_typ.ott')
| -rw-r--r-- | language/l2_typ.ott | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/language/l2_typ.ott b/language/l2_typ.ott index d55499e0..12baa059 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -201,8 +201,14 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} tinflist :: 'tinfs_' ::= {{ com In place so that a list of tinfs can be referred to without the dot form }} + | empty :: :: empty | tinf1 ... tinfn :: :: ls +conformsto :: 'conformsto_' ::= + {{ com how much conformance does overloading need }} + | full :: :: full + | parm :: :: parm + E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::= {{ phantom }} {{ hol tid |-> tinf}} {{ lem map tid tinf }} @@ -258,7 +264,7 @@ grammar | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} - | { id |-> overload tinf : tinf1 , ... , tinfn } :: :: overload + | { id |-> overload tinf conformsto : tinf1 , ... , tinfn } :: :: overload | ( E_t1 u+ .... u+ E_tn ) :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} |