blob: 4208c3e8e9b1b3bf5abc71d6afb71857cc5b42c6 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Arguments id {_} _.
Fail Record Functor (F : Type -> Type) := {
fmap : forall A B, (A -> B) -> F A -> F B;
fmap_identity : fmap _ _ id = id;
}.
Fail Inductive R (x:nat) := { y : R ltac:(clear x) }.
Inductive R (x:nat) := { y : bool; z : R _ }.
|
