 Timestamp:
 Apr 28, 2011, 10:55:47 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r761 r779 100 100 ] 101 101 qed. 102 103 let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝ 104 match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with 105 [ Stub _ ⇒ λc. c 106  Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a  _ ⇒ Leaf ? l ] 107  Node p l r ⇒ 108 λc. 109 (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with 110 [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉)) 111  Stub _ ⇒ λprf. Node ? p l r 112  Leaf _ ⇒ λabsd. ? 113 ] (refl ? (S p))) 114 ]. 115 [1: 116 destruct(absd) 117 2,3: 118 @ injective_S 119 assumption 120 ] 121 qed.
Note: See TracChangeset
for help on using the changeset viewer.