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/extralib.ma

    r487 r535  
    331331].
    332332interpretation "integer multiplication" 'times x y = (Z_times x y).
    333 
     333(* Now in cerco/Util.ma
    334334(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
    335335notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    336336notation < "'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 }.
    337337interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
    338 
     338*)
    339339(* datatypes/list.ma *)
    340340
Note: See TracChangeset for help on using the changeset viewer.