From: Enrico Tassi Date: Sun, 19 Oct 2008 09:37:50 +0000 (+0000) Subject: grave notation mistake fixed X-Git-Tag: make_still_working~4662 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=93c69f48fd73b111cb8e7f6cc78779790681e530;p=helm.git grave notation mistake fixed --- diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index aa7b7aff6..2296666c7 100644 --- a/helm/software/matita/contribs/didactic/induction.ma +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -190,7 +190,7 @@ let rec sem (v: nat → nat) (F: Formula) on F ≝ *) 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 90 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 90 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 90 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 < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }.