Stefan pushed to branch master at Stefan / Typer

Commits: f2b81386 by Stefan Monnier at 2020-04-02T19:31:41-04:00 * src/elab.ml (meta_to_var): Fix debruijn error.

* btl/pervasive.typer (Decidable): Make it universe-polymorphic. * src/builtin.ml (register_builtin_csts): Fix Type0 typo.

- - - - -

3 changed files:

- btl/pervasive.typer - src/builtin.ml - src/elab.ml

Changes:

===================================== btl/pervasive.typer ===================================== @@ -446,7 +446,7 @@ Not prop = prop -> False; %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't %% want that. -Decidable = typecons (Decidable (prop : Type)) +Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop));

%% Testing generalization in inductive type constructors.

===================================== src/builtin.ml ===================================== @@ -155,7 +155,7 @@ let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; - add_builtin_cst "Type0" DB.type1; + add_builtin_cst "Type0" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer;

===================================== src/elab.ml ===================================== @@ -356,7 +356,7 @@ let rec meta_to_var ids o (e : lexp) = -> let o' = o' - 1 in (o', (ak, v, meta_to_var ids (o' + o) t) :: fields)) - fields (flen, []) in + fields (flen + alen, []) in nfields) cases in mkInductive (l, label, nargs, ncases)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f2b81386a4aa31b49e0fd7e00ea7aea74c...