Changeset 268


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

Legend:

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

    r264 r268  
    22include "BitVectorTrie.ma".
    33include "String.ma".
    4 
    5 interpretation "Cartesian" 'product A B = (Cartesian A B).
    6 notation "hvbox(a break ⊎ b)"
    7  left associative with precedence 50
    8 for @{ 'disjoint_union $a $b }.
    9 interpretation "Either" 'disjoint_union A B = (Either A B).
    10 interpretation "Bool" 'or a b = (inclusive_disjunction a b).
    114
    125ninductive addressing_mode: Type[0] ≝
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

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

    r260 r268  
    4444    ].
    4545
     46interpretation "Bool" 'or a b = (inclusive_disjunction a b).
     47
    4648nlet rec negation (b: Bool) on b ≝
    4749  match b with
  • Deliverables/D4.1/Matita/Cartesian.ma

    r246 r268  
    22
    33nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
    4 {
    5   first: A;
     4{ first: A;
    65  second: B
    76}.
    87
    9 notation "(l,r)"
    10   non associative with precedence 90
    11   for @{ 'cartesian $l $r }.
    12  
    13 interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r).
     8interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
     9interpretation "Cartesian" 'product A B = (Cartesian A B).
  • Deliverables/D4.1/Matita/Connectives.ma

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

    r260 r268  
    77  Left: A → Either A B
    88| Right: B → Either A B.
     9
     10notation "hvbox(a break ⊎ b)"
     11 left associative with precedence 50
     12for @{ 'disjoint_union $a $b }.
     13interpretation "Either" 'disjoint_union A B = (Either A B).
    914
    1015ndefinition is_left ≝
  • Deliverables/D4.1/Matita/Exponential.ma

    r263 r268  
    55include "Nat.ma".
    66
    7 include "Equality.ma".
     7include "Plogic/equality.ma".
    88include "Connectives.ma".
    99
  • Deliverables/D4.1/Matita/Plogic/equality.ma

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

    r266 r268  
    55
    66include "Util.ma".
    7 
    8 include "Universes.ma".
    97
    108include "Nat.ma".
     
    133131    ].
    134132    //.
     133nqed.
     134
     135nlet rec split (A: Type[0]) (n,m: Nat) on m
     136             : Vector A (m+n) → (Vector A m) × (Vector A n)
     137
     138 match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with
     139  [ Z ⇒ λv.〈[[ ]], v〉
     140  | S m' ⇒ λv.
     141     match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
     142      [ Empty ⇒ λK.⊥
     143      | Cons o he tl ⇒ λK.
     144         match split A n m' (tl⌈Vector A (m'+n)↦Vector A o⌉) with
     145          [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
     146//; ndestruct; //.
    135147nqed.
    136148   
  • Deliverables/D4.1/Matita/depends

    r264 r268  
    11Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    2 Exponential.ma Connectives.ma Equality.ma Nat.ma
     2Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    33BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    44Cartesian.ma Universes.ma
     
    77Universes.ma
    88ASM.ma BitVectorTrie.ma Either.ma String.ma
    9 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     9Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1010Char.ma Universes.ma
    1111Connectives.ma Plogic/equality.ma
     
    2020Plogic/equality.ma Universes.ma
    2121Nat.ma Bool.ma Cartesian.ma Connectives.ma
    22 Equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.