diff options
| author | Kathy Gray | 2016-02-04 11:49:52 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-02-04 11:50:12 +0000 |
| commit | f3e01108eeb612a168f9ef4beac0b5747eeffbc8 (patch) | |
| tree | a17b33a9b24c76ae0e4e865a33d6fdcd3f8dc315 /src | |
| parent | 618df92d2a84832c978bc05f14c8611ded831abd (diff) | |
Relax constraints on quot temporarily since it was prohibiting negative numbers accidentally
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 26b68fa6..c85faba4 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1971,8 +1971,9 @@ let initial_typ_env = true, [Base(((mk_nat_params["n";"m";"o";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) - (mk_atom (mk_nv "o")))), - (External (Some "quot")),[GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one); + (mk_atom (mk_nv "o")))), + (*This should really be != to 0, as negative is just fine*) + (External (Some "quot")),[(*GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one);*) LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee, (mk_mult (mk_nv "n") (mk_nv "o")),(mk_nv "m"))], pure_e,pure_e,nob); |