diff options
| author | Christopher | 2015-12-21 00:26:05 +0100 |
|---|---|---|
| committer | Christopher | 2015-12-21 00:26:05 +0100 |
| commit | 3b2484a8d10a35b31b6071e39fd2c3018b007b46 (patch) | |
| tree | 5140f78857680aa6fce48fcff946e0773045f2a9 /src | |
| parent | ce7431d8e452952329439564969f8b592a01563b (diff) | |
| parent | f7a642bd3f8a5436873d0163114a30dad23ba9c2 (diff) | |
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 65727e1b..59a573d9 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2101,6 +2101,14 @@ let initial_typ_env = (mk_range n_zero (mk_nv "m"))]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), External (Some "bitwise_rotate"),[],pure_e,pure_e,nob)); + ("EXTS",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]), + (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")) + (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), + External (Some "EXTS"),[],pure_e,pure_e,nob)); + ("EXTZ",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]), + (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n")) + (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")), + External (Some "EXTZ"),[],pure_e,pure_e,nob)); ] |