blob: 1f2027d0619450cf1598e2cfdc535b40cdf60eb7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Inductive Foo := foo.
Declare Scope foo_scope.
Delimit Scope foo_scope with foo.
Bind Scope foo_scope with Foo.
Notation "'!'" := foo : foo_scope.
Definition of_foo {x : nat} {y : nat} (f : Foo) := f.
Notation a := (@of_foo O).
Notation b := (@a).
Check a !.
Check @a O !.
Check @b O.
Check @b O !. (* was failing *)
(* All are printed "a !", without making explicit the "0", which is
incidentally disputable *)
|
