Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (8 years ago)
Author:
campbell
Message:

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/Util.ma

    r534 r535  
    1313  ].
    1414   
     15(*
    1516notation "hvbox('if' b 'then' t 'else' f)"
    1617  non associative with precedence 83
    1718  for @{ 'if_then_else $b $t $f }.
     19*)
     20notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
     21notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    1822
    1923interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
Note: See TracChangeset for help on using the changeset viewer.