Quelle  bug_9329.v   Sprache: Coq

(* 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).