blob: aacc9df71e51d324ef9629f068808dd19613d404 (
plain)
1
2
3
4
5
|
(* Check that the nested inductive types positivity check avoids recursively
non uniform parameters (at least if these parameters break positivity) *)
Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
Fail Inductive u : Type := d : u | e : t u -> u.
|
