Closed janmasrovira closed 7 hours ago
The following should not pass the positivity test
module box; type Box (A : Type) := mkBox A; type P (A : Type) := mkP : (Box (P A) -> P A) -> P A;
The following should not pass the positivity test