Ignore:
Timestamp:
Dec 2, 2010, 2:03:48 PM (9 years ago)
Author:
mulligan
Message:

Resolved conflicts. Added new get_index' which hides the proof obligation of get_index_v. Needed a new lemma to typecheck it.

File:
1 edited

Legend:

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

    r362 r363  
    5858nqed.
    5959
     60ndefinition get_index' ≝
     61  λA: Type[0].
     62  λn, m: Nat.
     63  λb: Vector A (S (n + m)).
     64    get_index_v A (S (n + m)) b n ?.
     65  nnormalize;
     66  napply less_than_or_equal_monotone;
     67  napply less_than_or_equal_plus;
     68nqed.
     69
    6070nlet rec get_index_weak_v (A: Type[0]) (n: Nat)
    61                    (v: Vector A n) (m: Nat) on m ≝
     71                          (v: Vector A n) (m: Nat) on m ≝
    6272  match m with
    6373    [ Z ⇒
Note: See TracChangeset for help on using the changeset viewer.