Changeset 746 for src/utilities/BitVectorTrieSet.ma
 Timestamp:
 Apr 8, 2011, 11:51:38 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/BitVectorTrieSet.ma
r698 r746 1 1 include "ASM/BitVectorTrie.ma". 2 include "ASM/Util.ma". 2 3 3 4 definition BitVectorTrieSet ≝ BitVectorTrie unit. … … 50 51 qed. 51 52 53 let rec set_eq (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: bool ≝ 54 match b return λh. λ_. n = h → bool with 55 [ Stub s ⇒ 56 match c with 57 [ Stub s' ⇒ λ_. eq_nat s s' 58  _ ⇒ λ_. false 59 ] 60  Leaf l ⇒ 61 match c with 62 [ Leaf l' ⇒ λ_. true (* dpm: l and l' both unit *) 63  _ ⇒ λ_. false 64 ] 65  Node h l r ⇒ 66 match c with 67 [ Node h' l' r' ⇒ λprf. andb (set_eq h l ?) (set_eq h r ?) 68  _ ⇒ λ_. false 69 ] 70 ] (refl ? n). 71 [ 1: @ r 72  2: lapply (injective_S … prf) 73 # H 74 < H 75 @ r' 76 ] 77 qed. 78 79 (* 80 let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝ 81 match b with 82 [ Stub ⇒ 83 *) 84 52 85 definition set_insert ≝ 53 86 λn: nat. … … 57 90 58 91 definition set_empty ≝ λn. Stub unit n. 92 93 definition set_singleton ≝ 94 λn: nat. 95 λb: BitVector n. 96 insert unit n b it (set_empty ?).
Note: See TracChangeset
for help on using the changeset viewer.