blob: 03c60a8baa40ece0a2ece2c19976587102fe89a9 (
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).
Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
|
