Ignore:
Timestamp:
Nov 23, 2010, 12:56:26 PM (9 years ago)
Author:
mulligan
Message:

Need stronger set_ and get_index functions on vectors (current ones return a Maybe type).

File:
1 edited

Legend:

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

    r256 r259  
    5454interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    5555   
    56 nlet rec set_index (A: Type[0]) (n: Nat)
    57                    (v: Vector A n) (m: Nat) (a: A) on m ≝
     56nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) on m ≝
     57  match m return (λx. x < n → A) with
     58    [ Z ⇒
     59      match v with
     60        [ Empty ⇒ λ_.?
     61        | Cons p hd tl ⇒ λ_.hd
     62        ]
     63    | S o ⇒
     64      match v with
     65        [ Empty ⇒ λ_.?
     66        | Cons p hd tl ⇒ λprf: m < p. set_index A p tl o a
     67        ]
     68    ].
     69   
     70nlet rec set_index_weak (A: Type[0]) (n: Nat)
     71                        (v: Vector A n) (m: Nat) (a: A) on m ≝
    5872  match m with
    5973    [ Z ⇒
     
    6680        [ Empty ⇒ Nothing (Vector A n)
    6781        | Cons p hd tl ⇒
    68             let settail ≝ set_index A p tl o a in
     82            let settail ≝ set_index_weak A p tl o a in
    6983              match settail with
    7084                [ Nothing ⇒ Nothing (Vector A n)
Note: See TracChangeset for help on using the changeset viewer.