Changeset 320
 Timestamp:
 Nov 26, 2010, 6:13:26 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r315 r320 228 228 ]. 229 229 230 naxiom half_add:231 ∀n: Nat.232 ∀b, c: BitVector n.233 Bool × (BitVector n).234 235 230 naxiom full_add: 236 231 ∀n: Nat. … … 238 233 ∀d: Bit. 239 234 Bool × (BitVector n). 235 236 ndefinition half_add ≝ 237 λn: Nat. 238 λb, c: BitVector n. 239 full_add n b c false. 
Deliverables/D4.1/Matita/Vector.ma
r316 r320 159 159  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 160 160 ]. 161 162 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 163 (n: Nat) (m: Nat) 164 (f: A → B → C → C) (c: C) 165 (v: Vector A n) (q: Vector B m) on v ≝ 166 (match v return λx.λ_. x = m → C with 167 [ Empty ⇒ 168 match q return λx.λ_. Z = x → C with 169 [ Empty ⇒ λ_.c 170  Cons o hd tl ⇒ λabsd. ? 171 ] 172  Cons o hd tl ⇒ 173 match q return λx.λ_. S o = x → C with 174 [ Empty ⇒ λabsd. ? 175  Cons p hd' tl' ⇒ λprf: S o = S p. 176 fold_right_i A B C o p f (f hd hd') tl tl' 177 ] 178 ]) ?. 161 179 162 180 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.