diff options
| author | Gaëtan Gilbert | 2017-10-27 14:03:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 75508769762372043387c67a9abe94e8f940e80a (patch) | |
| tree | 3f63e7790e9f3b6e7384b0a445d62cfa7edbe829 /engine/eConstr.ml | |
| parent | a0e16c9e5c3f88a8b72935dd4877f13388640f69 (diff) | |
Add a non-cumulative impredicative universe SProp.
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index c7b092b114..521d6b707d 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -48,6 +48,7 @@ type 'a puniverses = 'a * EInstance.t let in_punivs a = (a, EInstance.empty) +let mkSProp = of_kind (Sort (ESorts.make Sorts.sprop)) let mkProp = of_kind (Sort (ESorts.make Sorts.prop)) let mkSet = of_kind (Sort (ESorts.make Sorts.set)) let mkType u = of_kind (Sort (ESorts.make (Sorts.sort_of_univ u))) @@ -81,6 +82,8 @@ let mkRef (gr,u) = let open GlobRef in match gr with | ConstructRef c -> mkConstructU (c,u) | VarRef x -> mkVar x +let type1 = mkSort Sorts.type1 + let applist (f, arg) = mkApp (f, Array.of_list arg) let applistc f arg = mkApp (f, Array.of_list arg) |