Ignore:
Timestamp:
Nov 30, 2010, 12:26:45 PM (9 years ago)
Author:
mulligan
Message:

Changes to execute_1 file. Changes to get everything type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r330 r337  
    2929(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3030
    31 ndefinition get_index
     31ndefinition get_index_bv
    3232  λn: Nat.
    3333  λb: BitVector n.
     
    3838interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
    3939   
    40 ndefinition set_index
     40ndefinition set_index_bv
    4141  λn: Nat.
    4242  λb: BitVector n.
     
    120120  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
    121121   
    122 ndefinition negation
     122ndefinition negation_bv
    123123  λn: Nat.
    124124  λb: BitVector n.
     
    131131(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    132132
    133 ndefinition rotate_left
    134   λm, n: Nat.
     133ndefinition rotate_left_bv
     134  λn, m: Nat.
    135135  λb: BitVector n.
    136136    rotate_left Bool n m b.
    137137
    138 ndefinition rotate_right
    139   λm, n: Nat.
     138ndefinition rotate_right_bv
     139  λn, m: Nat.
    140140  λb: BitVector n.
    141141    rotate_right Bool n m b.
    142142   
    143 ndefinition shift_left
    144   λm, n: Nat.
     143ndefinition shift_left_bv
     144  λn, m: Nat.
    145145  λb: BitVector n.
    146146  λc: Bool.
    147147    shift_left Bool n m b c.
    148148   
    149 ndefinition shift_right
    150   λm, n: Nat.
     149ndefinition shift_right_bv
     150  λn, m: Nat.
    151151  λb: BitVector n.
    152152  λc: Bool.
Note: See TracChangeset for help on using the changeset viewer.