-definition if : ∀A:Type.bool → A → A → A ≝
- λA,b,t,f. match b with [ true ⇒ t | false ⇒ f].
-
-notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }.
-notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }.
-interpretation "if" 'if a b c = (cic:/matita/test/russell/if.con _ a b c).
+notation > "'If' b 'Then' t 'Else' f" non associative
+with precedence 90 for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.