1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* NOTATION FOR MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1) ************)
17 (* Syntax extension *********************************************************)
20 non associative with precedence 90
23 notation "hvbox(T1 break ⤏ T2)"
24 right associative with precedence 65
25 for @{ 'TImp $T1 $T2 }.
27 notation "hvbox( L break Λ T )"
28 left associative with precedence 60
29 for @{ 'LAbst $L $T }.
31 notation "hvbox( L break Δ T )"
32 left associative with precedence 60
33 for @{ 'LAbbr $L $T }.
35 notation "hvbox( Λ T )"
36 non associative with precedence 65
39 (* Primitive global constants ***********************************************)
42 non associative with precedence 90
45 notation "hvbox( 𝕖𝕣 [ T ] )"
46 non associative with precedence 90
50 non associative with precedence 90
54 non associative with precedence 90
57 notation "hvbox( 𝕠𝕣 [ T1 , break T2 ] )"
58 non associative with precedence 90
59 for @{ 'ORec $T1 $T2 }.
62 non associative with precedence 90
66 non associative with precedence 90
69 notation "hvbox( 𝕤 [ T ] )"
70 non associative with precedence 90
73 notation "hvbox( 𝕟𝕣 [ T1 , break T2 , break T3 ] )"
74 non associative with precedence 90
75 for @{ 'NRec $T1 $T2 $3 }.
77 notation "hvbox( T1 ⊕ T2 )"
78 left associative with precedence 70
79 for @{ 'Sum $T1 $T2 }.
81 notation "hvbox( 𝕤𝕟 [ T ] )"
82 non associative with precedence 90
85 notation "hvbox( 𝕕𝕩 [ T ] )"
86 non associative with precedence 90
89 notation "hvbox( 𝕤𝕣 [ T1 , break T2 , break T3 ] )"
90 non associative with precedence 90
91 for @{ 'SRec $T1 $T2 $3 }.
94 non associative with precedence 90
98 non associative with precedence 90
101 notation "hvbox( 𝕠 )"
102 non associative with precedence 90
105 notation "hvbox( 𝕟 )"
106 non associative with precedence 90