Ignore:
Timestamp:
Dec 2, 2010, 11:53:49 AM (9 years ago)
Author:
sacerdot
Message:

Less ambiguous definitions.

File:
1 edited

Legend:

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

    r357 r362  
    3030interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
    3131
     32notation "hvbox(l break !!! break n)"
     33  non associative with precedence 90
     34  for @{ 'get_index_v $l $n }.
     35
    3236(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3337(* Lookup.                                                                    *)
    3438(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3539
    36 nlet rec get_index (A: Type[0]) (n: Nat)
     40nlet rec get_index_v (A: Type[0]) (n: Nat)
    3741                   (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
    3842  (match m with
     
    4549      (match v return λx.λ_. S o < x → A with
    4650        [ Empty ⇒ λprf: S o < Z. ?
    47         | Cons p hd tl ⇒ λprf: S o < S p. get_index A p tl o ?
     51        | Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
    4852        ])
    4953    ]) lt.
     
    5458nqed.
    5559
    56 nlet rec get_index_weak (A: Type[0]) (n: Nat)
     60nlet rec get_index_weak_v (A: Type[0]) (n: Nat)
    5761                   (v: Vector A n) (m: Nat) on m ≝
    5862  match m with
     
    6569      match v with
    6670        [ Empty ⇒ Nothing A
    67         | Cons p hd tl ⇒ get_index_weak A p tl o
    68         ]
    69     ].
    70    
    71 interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
     71        | Cons p hd tl ⇒ get_index_weak_v A p tl o
     72        ]
     73    ].
     74   
     75interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
    7276
    7377nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
Note: See TracChangeset for help on using the changeset viewer.