Ignore:
Timestamp:
Nov 23, 2010, 5:10:40 PM (9 years ago)
Author:
mulligan
Message:

Changes to bitvector.

File:
1 edited

Legend:

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

    r265 r266  
    8383interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    8484
    85 (*
    8685nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
    8786  (match m with
     
    10099    nassumption.
    101100nqed.
    102 *)
    103101   
    104102nlet rec set_index_weak (A: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.