Ignore:
Timestamp:
Nov 12, 2010, 4:01:48 PM (9 years ago)
Author:
mulligan
Message:

Strange problem with matita and the Maybe file? Cannot find Maybe.ng.

File:
1 edited

Legend:

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

    r234 r236  
    159159(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    160160
    161 nlet rec to_list (A: Type[0]) (n: Nat)
    162                  (v: Vector A n) on v ≝
    163   match v with
     161nlet rec list_of_vector (A: Type[0]) (n: Nat)
     162                        (v: Vector A n) on v ≝
     163  match v return λn.λv. List A with
    164164    [ Empty ⇒ cic:/matita/Cerco/List/List.con(0,1,1) A
    165     | Cons o hd tl ⇒ hd :: (to_list A o tl)
     165    | Cons o hd tl ⇒ cic:/matita/Cerco/List/List.con(0,2,1) A hd (list_of_vector A o tl)
    166166    ].
    167167
    168168(*
    169 nlet rec from_list (A: Type[0]) (l: List A) on l ≝
     169nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    170170  match l return λl. Vector A (length A l) with
    171171    [ Empty ⇒ cic:/matita/Cerco/Vector/Vector.con(0,1,1) A
Note: See TracChangeset for help on using the changeset viewer.