# Changeset 268 for Deliverables

Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (10 years ago)
Message:
• notation moved to proper places
• new function split on Vectors
Location:
Deliverables/D4.1/Matita
Files:
1 deleted
10 edited

Unmodified
Removed
• ## Deliverables/D4.1/Matita/ASM.ma

 r264 include "BitVectorTrie.ma". include "String.ma". interpretation "Cartesian" 'product A B = (Cartesian A B). notation "hvbox(a break ⊎ b)" left associative with precedence 50 for @{ 'disjoint_union \$a \$b }. interpretation "Either" 'disjoint_union A B = (Either A B). interpretation "Bool" 'or a b = (inclusive_disjunction a b). ninductive addressing_mode: Type[0] ≝
• ## Deliverables/D4.1/Matita/BitVectorTrie.ma

 r260 | Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) | Stub: ∀n: Nat. BitVectorTrie A n. notation "hvbox(t⌈h ↦ o⌉)" with precedence 45 for @{ match (? : \$o=\$h) with [ refl ⇒ \$t ] }. notation "⊥" with precedence 90 for @{ match ? in False with [ ] }. nlet rec lookup (A: Type[0]) (n: Nat)
• ## Deliverables/D4.1/Matita/Bool.ma

 r260 ]. interpretation "Bool" 'or a b = (inclusive_disjunction a b). nlet rec negation (b: Bool) on b ≝ match b with
• ## Deliverables/D4.1/Matita/Cartesian.ma

 r246 nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝ { first: A; { first: A; second: B }. notation "(l,r)" non associative with precedence 90 for @{ 'cartesian \$l \$r }. interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r). interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r). interpretation "Cartesian" 'product A B = (Cartesian A B).
• ## Deliverables/D4.1/Matita/Connectives.ma

 r260 ninductive Not (A:Prop): Prop ≝ nmk: (A → False) → Not A. notation "⊥" with precedence 90 for @{ match ? in False with [ ] }. interpretation "logical not" 'not x = (Not x).
• ## Deliverables/D4.1/Matita/Either.ma

 r260 Left: A → Either A B | Right: B → Either A B. notation "hvbox(a break ⊎ b)" left associative with precedence 50 for @{ 'disjoint_union \$a \$b }. interpretation "Either" 'disjoint_union A B = (Either A B). ndefinition is_left ≝
• ## Deliverables/D4.1/Matita/Exponential.ma

 r263 include "Nat.ma". include "Equality.ma". include "Plogic/equality.ma". include "Connectives.ma".
• ## Deliverables/D4.1/Matita/Plogic/equality.ma

 r260 ninductive eq (A:Type[2]) (x:A) : A → Prop ≝ refl: eq A x x. notation "hvbox(t⌈h ↦ o⌉)" with precedence 45 for @{ match (? : \$o=\$h) with [ refl ⇒ \$t ] }. interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
• ## Deliverables/D4.1/Matita/Vector.ma

 r266 include "Util.ma". include "Universes.ma". include "Nat.ma". ]. //. nqed. nlet rec split (A: Type[0]) (n,m: Nat) on m : Vector A (m+n) → (Vector A m) × (Vector A n) ≝ match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with [ Z ⇒ λv.〈[[ ]], v〉 | S m' ⇒ λv. match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with [ Empty ⇒ λK.⊥ | Cons o he tl ⇒ λK. match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. //; ndestruct; //. nqed.
• ## Deliverables/D4.1/Matita/depends

 r264 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma Exponential.ma Connectives.ma Equality.ma Nat.ma Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma Cartesian.ma Universes.ma Universes.ma ASM.ma BitVectorTrie.ma Either.ma String.ma Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma Char.ma Universes.ma Connectives.ma Plogic/equality.ma Plogic/equality.ma Universes.ma Nat.ma Bool.ma Cartesian.ma Connectives.ma Equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.