Changeset 244


Ignore:
Timestamp:
Nov 15, 2010, 10:42:20 AM (9 years ago)
Author:
mulligan
Message:

Vector.ma now compiles.

File:
1 edited

Legend:

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

    r243 r244  
    233233                        (v: Vector A n) on v ≝
    234234  match v return λn.λv. List A with
    235     [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/List/List/List.con(0,1,1) A)
     235    [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
    236236    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
    237237    ].
     
    241241nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    242242  match l return λl. Vector A (length A l) with
    243     [ Empty ⇒ ? (cic:/matita/Cerco/Datatypes/Listlike/Vector/Vector/Vector.con(0,1,1) A)
     243    [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
    244244    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
    245245    ].
Note: See TracChangeset for help on using the changeset viewer.