 Timestamp:
 Apr 28, 2011, 5:36:33 PM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r779 r782 8 8  Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) 9 9  Stub: ∀n: nat. BitVectorTrie A n. 10 11 axiom fold: 12 ∀A, B: Type[0]. 13 ∀n: nat. 14 ∀f: BitVector n → A → B → B. 15 ∀t: BitVectorTrie A n. 16 ∀b: B. 17 B. 10 18 11 19 let rec lookup_opt (A: Type[0]) (n: nat) 
src/ASM/Util.ma
r777 r782 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 5 lemma eq_rect_Type0_r : 6 ∀A: Type[0]. 7 ∀a:A. 8 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 9 #A #a #P #H #x #p 10 generalize in match H 11 generalize in match P 12 cases p 13 // 14 qed. 15 16 let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝ 17 match n return λo. o < length A l → A with 18 [ O ⇒ 19 match l return λm. 0 < length A m → A with 20 [ nil ⇒ λabsd1. ? 21  cons hd tl ⇒ λprf1. hd 22 ] 23  S n' ⇒ 24 match l return λm. S n' < length A m → A with 25 [ nil ⇒ λabsd2. ? 26  cons hd tl ⇒ λprf2. safe_nth A n' tl ? 27 ] 28 ] ?. 29 [ 1: 30 @ p 31  4: 32 normalize in prf2 33 normalize 34 @ le_S_S_to_le 35 assumption 36  2: 37 normalize in absd1; 38 cases (not_le_Sn_O O) 39 # H 40 elim (H absd1) 41  3: 42 normalize in absd2; 43 cases (not_le_Sn_O (S n')) 44 # H 45 elim (H absd2) 46 ] 47 qed. 4 48 5 49 let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ … … 128 172 129 173 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 130 131 lemma eq_rect_Type0_r :132 ∀A: Type[0].133 ∀a:A.134 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.135 #A #a #P #H #x #p136 generalize in match H137 generalize in match P138 cases p139 //140 qed.141 142 174 143 175 notation "hvbox(t⌈o ↦ h⌉)"
Note: See TracChangeset
for help on using the changeset viewer.