test-suite/success/custom_entry.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Declare Custom Entry foo.

Print Custom Grammar foo.

Notation "[ e ]" := e (e custom foo at level 0).

Print Custom Grammar foo.

Notation "1" := O (in custom foo at level 0).

Print Custom Grammar foo.

Fail Declare Custom Entry foo.