1 (* (C) 2014 Luca Bressan *)
3 notation "hvbox(a break \to b)"
4 right associative with precedence 20
5 for @{ \forall $_:$a.$b }.
7 notation < "hvbox(Σ ident i : ty break . p)"
8 left associative with precedence 20
9 for @{'sigma (λ${ident i}: $ty. $p) }.
10 notation < "hvbox(Σ ident i break . p)"
12 for @{'sigma (λ${ident i}. $p) }.
14 notation > "Σ list1 ident x sep , opt (: T). term 19 Px"
17 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}: $T. $acc)} } }
18 @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}. $acc)} } }
21 notation "hvbox(π1 s)"
22 non associative with precedence 70
24 notation "hvbox(π2 s)"
25 non associative with precedence 70
28 notation "hvbox(〈 term 19 a, break term 19 b 〉)"
29 with precedence 90 for @{ 'mk_sigma $a $b }.
31 notation "hvbox(B break × C)"
32 left associative with precedence 55
33 for @{ 'times $B $C }.
36 non associative with precedence 90
40 non associative with precedence 90
43 non associative with precedence 90
46 notation "hvbox(B break + C)"
47 left associative with precedence 50
51 non associative with precedence 90
54 notation "hvbox(B break ∨ C)"
55 left associative with precedence 50
58 notation "hvbox(B break ∧ C)"
59 left associative with precedence 60
62 notation < "hvbox(B break → C)"
63 left associative with precedence 60
64 for @{ 'implies $B $C }.
66 notation < "hvbox(∃ ident i : ty break . p)"
67 left associative with precedence 20
68 for @{'exists (λ${ident i}: $ty. $p) }.
69 notation < "hvbox(∃ ident i break . p)"
71 for @{'exists (λ${ident i}. $p) }.
73 notation > "∃ list1 ident x sep , opt (: T). term 19 Px"
76 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}: $T. $acc)} } }
77 @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}. $acc)} } }
79 notation "hvbox(« term 19 a, break term 19 b »)"
80 with precedence 90 for @{ 'mk_exists $a $b }.
83 non associative with precedence 90
86 notation "hvbox(a break = b)"
87 non associative with precedence 45
90 notation "hvbox(a break ≃ b)"
91 non associative with precedence 45
95 non associative with precedence 90
98 non associative with precedence 80
100 notation "hvbox(d break • d')"
101 left associative with precedence 60
102 for @{ 'tra $d $d' }.
104 notation "hvbox(y break ∘ d)"
105 non associative with precedence 50
106 for @{ 'subst $d $y }.
108 notation "hvbox(f ◽ d)"
109 non associative with precedence 40
111 notation "hvbox(f ˙ d)"
112 non associative with precedence 60
113 for @{ 'sup_f $f $d}.