Changeset 229 for Deliverables/D4.1/Matita/List.ma
- Timestamp:
- Nov 9, 2010, 5:00:50 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/List.ma
r228 r229 1 1 include "Maybe.ma". 2 2 include "Nat.ma". 3 include "Util.ma". 3 4 4 5 ninductive List (A: Type[0]): Type[0] ≝ … … 20 21 match l with 21 22 [ Empty ⇒ Z 22 | Cons hd tl ⇒ S (length A tl)23 | Cons hd tl ⇒ S $ length A tl 23 24 ]. 24 25 … … 65 66 match l with 66 67 [ 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) 68 69 ]. 69 70 … … 87 88 match n with 88 89 [ Z ⇒ Empty A 89 | S o ⇒ a :: (replicate A o a)90 | S o ⇒ a :: replicate A o a 90 91 ].
Note: See TracChangeset
for help on using the changeset viewer.