Changeset 260 for Deliverables/D4.1/Matita/BitVectorTrie.ma

Timestamp:

Nov 23, 2010, 2:30:10 PM (11 years ago)

Author:

sacerdot

Message:

• Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
• ambiguity reduced by lower-casing booleans

File:

• Deliverables/D4.1/Matita/BitVectorTrie.ma (modified) (4 diffs)

Deliverables/D4.1/Matita/BitVectorTrie.ma

@@ -1 +1 @@
 include "BitVector.ma".
-include "Compare.ma".
+(*include "Compare.ma".*)
 include "Bool.ma".
 include "Maybe.ma".
@@ -31 +31 @@
         | Node h l r ⇒
            match hd with
-             [ True ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
-             | False ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
+             [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
+             | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
              ]
         | Stub s ⇒ λ_. a
@@ -47 +47 @@
     | Cons o hd tl ⇒
       match hd with
-        [ True ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
-        | False ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
+        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
+        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
         ]
     ].
@@ -62 +62 @@
             | Node p l r ⇒ λprf.
                match hd with
-                [ True ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
-                | False ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
+                [ true ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
+                | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
                 ]
             | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a)