aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/inductive3.v
blob: e5a4e1b66cd9ae0b71e9aa7b915369f2df869eb5 (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.
Inductive u : Type := d : u | e : t u -> u.