blob: ba7a5c98fc90ba8d2532726db4a28e85d3a05244 (
plain)
1
2
3
4
5
6
7
8
|
Notation bar := $(exact I)$.
Notation foo := bar (only parsing).
Class baz := { x : False }.
Instance: baz.
Admitted.
Definition baz0 := ((_ : baz) = (_ : baz)).
Definition foo1 := (foo = foo).
Fail Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
|
