Ignore:
Timestamp:
Nov 30, 2010, 2:36:20 PM (9 years ago)
Author:
sacerdot
Message:

::: is now used in place of :: for vectors to reduce ambiguity

File:
1 edited

Legend:

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

    r329 r340  
    2828  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
    2929
     30notation "hvbox(hd break ::: tl)"
     31  right associative with precedence 52
     32  for @{ 'vcons $hd $tl }.
     33
    3034interpretation "Vector vnil" 'vnil = (Empty ?).
    3135interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
    32 interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
    3336
    3437(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    7881      match v return λx.λ_. Z < x → Vector A x with
    7982        [ Empty ⇒ λabsd1: Z < Z. Empty A
    80         | Cons p hd tl ⇒ λprf1: Z < S p. (a :: tl)
     83        | Cons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
    8184        ]
    8285    | S o ⇒
    8386      (match v return λx.λ_. S o < x → Vector A x with
    8487        [ Empty ⇒ λprf: S o < Z. Empty A
    85         | Cons p hd tl ⇒ λprf: S o < S p. hd :: (set_index A p tl o a ?)
     88        | Cons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
    8689        ])
    8790    ]) lt.
     
    135138      | Cons o he tl ⇒ λK.
    136139         match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with
    137           [ mk_Cartesian v1 v2 ⇒ 〈he::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
     140          [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    138141//; ndestruct; //.
    139142nqed.
     
    200203  match v with
    201204    [ Empty ⇒ Empty B
    202     | Cons n hd tl ⇒ (f hd) :: (map A B n f tl)
     205    | Cons n hd tl ⇒ (f hd) ::: (map A B n f tl)
    203206    ].
    204207
     
    212215        | Cons m hd' tl' ⇒
    213216            λe: S n = S m.
    214               (f hd hd') :: (zip_with A B C n f tl ?)
     217              (f hd hd') ::: (zip_with A B C n f tl ?)
    215218        ]
    216219    ])
     
    240243  match n return λn. Vector A n with
    241244    [ Z ⇒ Empty A
    242     | S m ⇒ h :: (replicate A m h)
     245    | S m ⇒ h ::: (replicate A m h)
    243246    ].
    244247
     
    247250  match v return (λn.λv. Vector A (n + m)) with
    248251    [ Empty ⇒ q
    249     | Cons o hd tl ⇒ hd :: (append A o m tl q)
     252    | Cons o hd tl ⇒ hd ::: (append A o m tl q)
    250253    ].
    251254   
     
    258261nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
    259262                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
    260   a ::
     263  a :::
    261264    (match v with
    262265       [ Empty ⇒ Empty A
     
    310313  match l return λl. Vector A (length A l) with
    311314    [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
    312     | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
     315    | Cons hd tl ⇒ ? (hd ::: (vector_of_list A tl))
    313316    ].
    314317    nnormalize.
Note: See TracChangeset for help on using the changeset viewer.