Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (9 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:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r248 r260  
    11include "BitVector.ma".
    2 include "Compare.ma".
     2(*include "Compare.ma".*)
    33include "Bool.ma".
    44include "Maybe.ma".
     
    3131        | Node h l r ⇒
    3232           match hd with
    33              [ True ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
    34              | False ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
     33             [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
     34             | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
    3535             ]
    3636        | Stub s ⇒ λ_. a
     
    4747    | Cons o hd tl ⇒
    4848      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)
    5151        ]
    5252    ].
     
    6262            | Node p l r ⇒ λprf.
    6363               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⌉)
    6666                ]
    6767            | Stub p ⇒ λprf. ? (prepare_trie_for_insertion A ? b a)
Note: See TracChangeset for help on using the changeset viewer.