Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (10 years ago)
Author:
sacerdot
Message:
  • notation moved to proper places
  • new function split on Vectors
File:
1 edited

Legend:

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

    r260 r268  
    88| Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    99| Stub: ∀n: Nat. BitVectorTrie A n.
    10 
    11 notation "hvbox(t⌈h ↦ o⌉)"
    12   with precedence 45
    13   for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
    14 
    15 notation "⊥" with precedence 90
    16   for @{ match ? in False with [ ] }.
    1710
    1811nlet rec lookup (A: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.