Changeset 260 for Deliverables/D4.1/Matita/BitVectorTrie.ma
- Timestamp:
- Nov 23, 2010, 2:30:10 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/BitVectorTrie.ma
r248 r260 1 1 include "BitVector.ma". 2 include "Compare.ma". 2 (*include "Compare.ma".*) 3 3 include "Bool.ma". 4 4 include "Maybe.ma". … … 31 31 | Node h l r ⇒ 32 32 match hd with 33 [ True ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a34 | False ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a33 [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a 34 | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a 35 35 ] 36 36 | Stub s ⇒ λ_. a … … 47 47 | Cons o hd tl ⇒ 48 48 match hd with 49 [ True ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)50 | False ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)49 [ true ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a) 50 | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o) 51 51 ] 52 52 ]. … … 62 62 | Node p l r ⇒ λprf. 63 63 match hd with 64 [ True ⇒ Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))65 | False ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)64 [ true ⇒ Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉)) 65 | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉) 66 66 ] 67 67 | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a)
Note: See TracChangeset
for help on using the changeset viewer.