Changeset 1393 for src/ASM/Status.ma


Ignore:
Timestamp:
Oct 17, 2011, 3:50:50 PM (8 years ago)
Author:
boender
Message:
  • added invariant for policy trie to assembly
  • change (syntax only) to status in order to make it compile
  • added lemma + renaming to bitvectortrie
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r993 r1393  
    970970        λbit_addr: True.
    971971          let 〈 nu, nl 〉 ≝ split … 4 4 b in
    972           let bit_1 ≝ get_index_v nu 0 ? in
     972          let bit_1 ≝ get_index_v ? ? nu 0 ? in
    973973          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    974974            match bit_1 with
     
    989989        λn_bit_addr: True.
    990990          let 〈 nu, nl 〉 ≝ split … 4 4 n in
    991           let bit_1 ≝ get_index_v nu 0 ? in
     991          let bit_1 ≝ get_index_v ? ? nu 0 ? in
    992992          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    993993            match bit_1 with
Note: See TracChangeset for help on using the changeset viewer.