X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fconnectives.ma;h=34661dc8015e62a19403fb16e337359acb59c19e;hb=a5a3d944e528c6006f0ea901dded7c79367adb75;hp=25fb2ce93c38784c9069fe19dcf8e01551e5275a;hpb=5799dca87fe5c1b5a3cc1f4869109fe75d055ecd;p=helm.git diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma index 25fb2ce93..34661dc80 100644 --- a/helm/software/matita/nlibrary/logic/connectives.ma +++ b/helm/software/matita/nlibrary/logic/connectives.ma @@ -14,28 +14,48 @@ include "logic/pts.ma". -ninductive True: CProp ≝ +ninductive True: CProp[0] ≝ I : True. -ninductive False: CProp ≝. +ninductive False: CProp[0] ≝. -ndefinition Not: CProp → CProp ≝ +ndefinition Not: CProp[0] → CProp[0] ≝ λA. A → False. interpretation "logical not" 'not x = (Not x). -ninductive And (A,B:CProp) : CProp ≝ +ninductive And (A,B:CProp[0]) : CProp[0] ≝ conj : A → B → And A B. interpretation "logical and" 'and x y = (And x y). -ninductive Or (A,B:CProp) : CProp ≝ +ninductive Or (A,B:CProp[0]) : CProp[0] ≝ or_introl : A → Or A B | or_intror : B → Or A B. interpretation "logical or" 'or x y = (Or x y). -ninductive Ex (A:Type) (P:A → CProp) : CProp ≝ +ninductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝ ex_intro: ∀x:A. P x → Ex A P. + +ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝ + ex_intro1: ∀x:A. P x → Ex1 A P. + +interpretation "exists1" 'exists x = (Ex1 ? x). interpretation "exists" 'exists x = (Ex ? x). + +nrecord iff (A,B: CProp[0]) : CProp[0] ≝ + { if: A → B; + fi: B → A + }. + +notation > "hvbox(a break \liff b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +notation "hvbox(a break \leftrightarrow b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +interpretation "logical iff" 'iff x y = (iff x y).