diff options
| author | Kathy Gray | 2015-12-17 16:48:54 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-12-17 16:48:54 +0000 |
| commit | f7a642bd3f8a5436873d0163114a30dad23ba9c2 (patch) | |
| tree | 64a4fda4cd0ddd6e8af9521aaeda9cadf8919828 /src | |
| parent | 0b940fb7c599e2e47cc21a2708d4cae13cb1d934 (diff) | |
Remove external functions that the library provides, having added them to the type environment finally.
(Also small cleaning of the new makefile)
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)); ] |