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

More changes.

File:
1 edited

Legend:

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

    r228 r229  
    11include "Maybe.ma".
    22include "Nat.ma".
     3include "Util.ma".
    34
    45ninductive List (A: Type[0]): Type[0] ≝
     
    2021  match l with
    2122    [ Empty ⇒ Z
    22     | Cons hd tl ⇒ S (length A tl)
     23    | Cons hd tl ⇒ S $ length A tl
    2324    ].
    2425   
     
    6566  match l with
    6667    [ Empty ⇒ Empty A
    67     | Cons hd tl ⇒ reverse A tl @ (Cons A hd (Empty A))
     68    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    6869    ].
    6970   
     
    8788  match n with
    8889    [ Z ⇒ Empty A
    89     | S o ⇒ a :: (replicate A o a)
     90    | S o ⇒ a :: replicate A o a
    9091    ].
Note: See TracChangeset for help on using the changeset viewer.