Ignore:
Timestamp:
Jul 4, 2011, 3:31:18 PM (8 years ago)
Author:
mulligan
Message:

removed offsets after reading cerco mailing list

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1044 r1052  
    111111  | Stub _ ⇒ λ_.None ?
    112112  ]) b.
     113
     114definition member ≝
     115  λA.
     116  λn.
     117  λb: BitVector n.
     118  λt: BitVectorTrie A n.
     119  match lookup_opt A n b t with
     120  [ None ⇒ false
     121  | _    ⇒ true
     122  ].
     123
     124definition member_p ≝
     125  λA.
     126  λn.
     127  λb: BitVector n.
     128  λt: BitVectorTrie A n.
     129  match lookup_opt A n b t with
     130  [ None ⇒ False
     131  | _    ⇒ True
     132  ].
    113133 
    114134lemma forall_lookup:
Note: See TracChangeset for help on using the changeset viewer.