@@ -53,8+53,8 @@ interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \e
(* USARE L'ESISTENZIALE DEBOLE *)
definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
(* USARE L'ESISTENZIALE DEBOLE *)
definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation > "'If' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+notation < "'If' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.
interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.