Changeset 744 for src/common/Mem.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r718 r744  
    623623    ]
    624624]
    625 %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval | 3: @Hnext ]
     625%2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl'
     626[ @(absurd ? Hcl' Hcl) | @(absurd ? Hal' Hal) | @(absurd ? Hhi' Hhi)
     627| @(absurd ? Hlo' Hlo) | @(absurd ? Hval Hnext) ]
    626628qed.
    627629
Note: See TracChangeset for help on using the changeset viewer.