diff options
| author | Gabriel Kerneis | 2014-07-04 15:18:04 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-07-04 15:18:04 +0100 |
| commit | aa9440f5132008926624f2f00d5c4044734d80ac (patch) | |
| tree | a33d91fa6f6acb13c2077456e8195ad6e6d5fc37 /src | |
| parent | 04934f061ed5dac10d112bdfd3fcbec7e8849dc3 (diff) | |
Relax constraints for quot_vec
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 72d58728..2279418f 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -924,11 +924,11 @@ let initial_typ_env = LtEq(Specc(Parse_ast.Int("quot",None)), (mk_mult (mk_add (mk_nv "o") (mk_nv "p")) (mk_add (mk_nv "q") (mk_nv "r"))), (mk_add (mk_nv "n") (mk_nv "m")))],pure_e); - Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), + Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); - mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")]) + mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), - External (Some "quot_vec"),[],pure_e)])); + External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e)])); (* incorrect types, not pressing as the type checker puts in the correct types automatically on a first pass *) ("to_num_inc",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,false,pure_e)}),External None,[],pure_e)); ("to_num_dec",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,false,pure_e)}),External None,[],pure_e)); |