Ignore:
Timestamp:
Apr 28, 2011, 5:36:33 PM (9 years ago)
Author:
mulligan
Message:

More work on rtl-ertl pass from today, plus resolved conflict.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r779 r782  
    88| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    99| Stub: ∀n: nat. BitVectorTrie A n.
     10
     11axiom fold:
     12 ∀A, B: Type[0].
     13 ∀n: nat.
     14 ∀f: BitVector n → A → B → B.
     15 ∀t: BitVectorTrie A n.
     16 ∀b: B.
     17   B.
    1018
    1119let rec lookup_opt (A: Type[0]) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.