diff options
Diffstat (limited to 'language/l2_typ.ott')
| -rw-r--r-- | language/l2_typ.ott | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 43a3ea17..057ddfba 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -47,6 +47,7 @@ t , u :: 'T_' ::= | t1 -> t2 effect :: :: fn | ( t1 * .... * tn ) :: :: tup | id t_args :: :: app + | t |-> t1 :: :: abbrev | register t_args :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }} | t [ t1 / id1 ... tn / idn ] :: M :: subst {{ ichlo "todo" }} |