Changeset 329 for Deliverables/D4.1/Matita/List.ma
 Timestamp:
 Nov 29, 2010, 1:42:00 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/List.ma
r260 r329 7 7 include "Bool.ma". 8 8 include "Nat.ma". 9 (* include "Maybe.ma". *) 9 include "Maybe.ma". 10 10 include "Plogic/equality.ma". 11 11 … … 38 38 39 39 (* ===================================== *) 40 (* Building lists from scratch *) 41 (* ===================================== *) 42 43 nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝ 44 match n with 45 [ Z ⇒ Empty A 46  S o ⇒ a :: replicate A o a 47 ]. 48 49 nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝ 50 match l with 51 [ Empty ⇒ m 52  Cons hd tl ⇒ hd :: (append A tl m) 53 ]. 54 55 notation "hvbox(l break @ r)" 56 right associative with precedence 47 57 for @{ 'append $l $r }. 58 59 interpretation "List append" 'append = (append ?). 60 61 (* ===================================== *) 62 (* Other manipulations. *) 63 (* ===================================== *) 64 65 nlet rec length (A: Type[0]) (l: List A) on l ≝ 66 match l with 67 [ Empty ⇒ Z 68  Cons hd tl ⇒ S $ length A tl 69 ]. 70 71 nlet rec reverse (A: Type[0]) (l: List A) on l ≝ 72 match l with 73 [ Empty ⇒ Empty A 74  Cons hd tl ⇒ reverse A tl @ (hd :: Empty A) 75 ]. 76 77 (* ===================================== *) 40 78 (* Lookup. *) 41 79 (* ===================================== *) 42 43 (* 44 nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝ 80 81 nlet rec get_index (A: Type[0]) (l: List A) 82 (n: Nat) (lt: n < length ? l) on n: A ≝ 83 match n return λx. x < length ? l → A with 84 [ Z ⇒ 85 match l return λx. Z < length ? x → A with 86 [ Empty ⇒ λabsd: Z < Z. ? 87  Cons hd tl ⇒ λp. hd 88 ] 89  S o ⇒ 90 match l return λx. S o < length ? x → A with 91 [ Empty ⇒ λabsd: S o < Z. ? 92  Cons hd tl ⇒ λp. get_index A tl o ? 93 ] 94 ] ?. 95 ##[##1: 96 nassumption; 97 ####2: 98 ncases (nothing_less_than_Z Z); 99 #K; 100 ncases (K absd); 101 ####3: 102 ncases (nothing_less_than_Z (S o)); 103 #K; 104 ncases (K absd); 105 ## ncases (less_than_monoton); 106 107 108 nlet rec get_index_weak (A: Type[0]) (l: List A) (n: Nat) on n ≝ 45 109 match n with 46 110 [ Z ⇒ … … 58 122 interpretation "List get_index" 'get_index l n = (get_index ? l n). 59 123 60 nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝124 nlet rec set_index_weak (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝ 61 125 match n with 62 126 [ Z ⇒ … … 85 149  Cons hd tl ⇒ drop A tl o 86 150 ] 87 ]. 88 *) 89 90 (* ===================================== *) 91 (* Building lists from scratch *) 92 (* ===================================== *) 93 94 nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝ 95 match n with 96 [ Z ⇒ Empty A 97  S o ⇒ a :: replicate A o a 98 ]. 99 100 nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝ 101 match l with 102 [ Empty ⇒ m 103  Cons hd tl ⇒ hd :: (append A tl m) 104 ]. 105 106 notation "hvbox(l break @ r)" 107 right associative with precedence 47 108 for @{ 'append $l $r }. 109 110 interpretation "List append" 'append = (append ?). 111 112 (* ===================================== *) 113 (* Other manipulations. *) 114 (* ===================================== *) 115 116 nlet rec length (A: Type[0]) (l: List A) on l ≝ 117 match l with 118 [ Empty ⇒ Z 119  Cons hd tl ⇒ S $ length A tl 120 ]. 121 122 nlet rec reverse (A: Type[0]) (l: List A) on l ≝ 123 match l with 124 [ Empty ⇒ Empty A 125  Cons hd tl ⇒ reverse A tl @ (hd :: Empty A) 126 ]. 151 ]. 127 152 128 153 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.