Changeset 223


Ignore:
Timestamp:
Nov 8, 2010, 2:24:56 PM (9 years ago)
Author:
mulligan
Message:

File for bitvector specific stuff added.

Location:
Deliverables/D4.1/Matita
Files:
1 added
1 edited

Legend:

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

    r222 r223  
    4040    ].
    4141   
     42(*   
    4243nlet rec append (A: Type[0]) (n: nat) (m: nat)
    4344                (v: Vector A n) (q: Vector A m) on v ≝
    4445  match v with
    4546    [ Empty ⇒ q
    46     | Cons n hd tl ⇒ Cons n hd (append A n m tl q)
     47    | Cons n hd tl ⇒ Cons ? n hd (append A n m tl q)
    4748    ].
     49*)
    4850
    4951(*   
Note: See TracChangeset for help on using the changeset viewer.