blob: d198d45f2f16186e82ebe29ad75d3316f3c31467 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Declare Custom Entry atom.
Notation "1" := tt (in custom atom).
Notation "atom:( s )" := s (s custom atom).
Declare Custom Entry expr.
Notation "expr:( s )" := s (s custom expr).
Notation "( x , y , .. , z )" := (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..))
(in custom expr at level 0, x custom atom, y custom atom, z custom atom).
Check atom:(1).
Check expr:((1,1)).
Check expr:((1,1,1)).
|
