diff options
Diffstat (limited to 'language/l2_typ.ott')
| -rw-r--r-- | language/l2_typ.ott | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 5c17c3f6..65857331 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -50,8 +50,11 @@ t , u :: 'T_' ::= | t |-> t1 :: :: abbrev | register < t_arg > :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }} | range < ne ne' > :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }} - | vector < ne ne' ord t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} + | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} + | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} | bit :: S :: bit_typ {{ ichlo T_id "bit" }} + | string :: S :: string_typ {{ ichlo T_id "string" }} + | unit :: S :: unit_typ {{ ichlo T_id "unit" }} | t [ t_arg1 / tid1 .. t_argn / tidn ] :: M :: subst {{ ichlo "todo" }} optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} |