blob: f24d13b8af255ec6fac6867a8b38f77e06b3d056 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* variances other than Invariant are forbidden for non-cumul inductives *)
Fail Inductive foo@{+u} : Prop := .
Fail Polymorphic Inductive foo@{*u} : Prop := .
Inductive foo@{=u} : Prop := .
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Inductive force_invariant@{=u} : Prop := .
Fail Definition lift@{u v | u < v} (x:force_invariant@{u}) : force_invariant@{v} := x.
Inductive force_covariant@{+u} : Prop := .
Fail Definition lift@{u v | v < u} (x:force_covariant@{u}) : force_covariant@{v} := x.
Definition lift@{u v | u < v} (x:force_covariant@{u}) : force_covariant@{v} := x.
Fail Inductive not_irrelevant@{*u} : Prop := nirr (_ : Type@{u}).
Inductive check_covariant@{+u} : Prop := cov (_ : Type@{u}).
Fail Inductive not_covariant@{+u} : Prop := ncov (_ : Type@{u} -> nat).
|
