Changeset 328
- Timestamp:
- Nov 29, 2010, 11:17:58 AM (10 years ago)
- Location:
- Deliverables/D4.1/Matita
- Files:
-
- 1 added
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Plogic/equality.ma
r268 r328 32 32 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. 33 33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption. 34 nqed. 35 36 nlemma eq_rect_Type0_r : 37 ∀A: Type[0]. 38 ∀a:A. 39 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 40 #A a P H x p. 41 ngeneralize in match H. 42 ngeneralize in match P. 43 ncases p. 44 //. 34 45 nqed. 35 46 -
Deliverables/D4.1/Matita/Vector.ma
r322 r328 170 170 ]. 171 171 172 (*173 172 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 174 (n: Nat) (m: Nat) 175 (f: A → B → C → C) (c: C) 176 (v: Vector A n) (q: Vector B m) on v ≝ 177 (match v return λx.λ_. x = m → C with 173 (n: Nat) (f: A → B → C → C) (c: C) 174 (v: Vector A n) (q: Vector B n) on v ≝ 175 (match v return λx.λ_. x = n → C with 178 176 [ Empty ⇒ 179 177 match q return λx.λ_. Z = x → C with 180 [ Empty ⇒ λ _.c178 [ Empty ⇒ λprf: Z = Z. c 181 179 | Cons o hd tl ⇒ λabsd. ? 182 180 ] 183 181 | Cons o hd tl ⇒ 184 182 match q return λx.λ_. S o = x → C with 185 [ Empty ⇒ λabsd . ?183 [ Empty ⇒ λabsd: S o = Z. ? 186 184 | Cons p hd' tl' ⇒ λprf: S o = S p. 187 fold_right_i A B C o p f (f hd hd') tl tl' 188 ] 189 ]) ?. 190 *) 185 fold_right_i A B C o f (f hd hd' c) tl ? 186 ] 187 ]) (refl ? n). 188 ##[##1,2: 189 ndestruct; 190 ##| ndestruct (prf); 191 napply tl'; 192 ##] 193 nqed. 191 194 192 195 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) … … 207 210 | Cons n hd tl ⇒ (f hd) :: (map A B n f tl) 208 211 ]. 209 210 (* Should be moved into Plogic/equality.ma at some point. Only Type[2] version211 currently in there.212 *)213 nlemma eq_rect_Type0_r :214 ∀A: Type[0].215 ∀a:A.216 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.217 #A a P H x p.218 ngeneralize in match H.219 ngeneralize in match P.220 ncases p.221 //.222 nqed.223 212 224 213 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat) … … 477 466 @. 478 467 nqed. 479 480 naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool. -
Deliverables/D4.1/Matita/depends
r316 r328 1 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 1 3 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma3 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma4 4 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma 5 5 Cartesian.ma Universes.ma 6 Universes.ma 6 7 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma 7 8 Either.ma Bool.ma Maybe.ma Universes.ma 8 Universes.ma9 9 ASM.ma BitVectorTrie.ma Either.ma String.ma 10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma11 10 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 12 11 Char.ma Universes.ma 12 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma 13 13 Connectives.ma Plogic/equality.ma 14 14 Bool.ma Universes.ma … … 16 16 List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma 17 17 Util.ma Nat.ma 18 Compare.ma Universes.ma 18 19 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma 19 Compare.ma Universes.ma20 20 String.ma Char.ma List.ma 21 21 Plogic/equality.ma Universes.ma
Note: See TracChangeset
for help on using the changeset viewer.