1
2
3
4
5
6
7
8
9
10
11
12
|
(* Declare empty levels in the same order they are computed *)
Notation "< a ; b ; c >1" :=
(sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21).
Notation "< a ; b ; c >2" :=
(sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31).
Notation "< a ; b ; c >3" :=
(sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41).
Notation "< a ; b ; c >4" :=
(sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49).
Notation "< a ; b >" :=
(sum a b) (at level 61, a at level 63, b at level 62).
|
