Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (9 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File:
1 edited

Legend:

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

    r259 r260  
    1212include "Cartesian.ma".
    1313include "Maybe.ma".
    14 include "Equality.ma".
     14include "Plogic/equality.ma".
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    244244                        (v: Vector A n) on v ≝
    245245  match v return λn.λv. List A with
    246     [ Empty ⇒ ? (cic:/matita/Cerco/List/List.con(0,1,1) A)
     246    [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
    247247    | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
    248248    ].
     
    252252nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    253253  match l return λl. Vector A (length A l) with
    254     [ Empty ⇒ ? (cic:/matita/Cerco/Vector/Vector.con(0,1,1) A)
     254    [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
    255255    | Cons hd tl ⇒ ? (hd :: (vector_of_list A tl))
    256256    ].
Note: See TracChangeset for help on using the changeset viewer.