Changeset 268 for Deliverables/D4.1/Matita/BitVectorTrie.ma
 Timestamp:
 Nov 23, 2010, 5:44:42 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVectorTrie.ma
r260 r268 8 8  Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) 9 9  Stub: ∀n: Nat. BitVectorTrie A n. 10 11 notation "hvbox(t⌈h ↦ o⌉)"12 with precedence 4513 for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.14 15 notation "⊥" with precedence 9016 for @{ match ? in False with [ ] }.17 10 18 11 nlet rec lookup (A: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.