Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (9 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r698 r726  
    77| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    88| Stub: ∀n: nat. BitVectorTrie A n.
     9
     10let rec lookup_opt (A: Type[0]) (n: nat)
     11                (b: BitVector n) (t: BitVectorTrie A n) on t
     12       : option A ≝
     13 (match t return λx.λ_. BitVector x → option A with
     14  [ Leaf l ⇒ λ_.Some ? l
     15  | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l)
     16  | Stub _ ⇒ λ_.None ?
     17  ]) b.
    918
    1019let rec lookup (A: Type[0]) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.