Changeset 1890 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Apr 18, 2012, 2:01:46 PM (8 years ago)
Author:
boender
Message:
  • added comment about bitvector translation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r1635 r1890  
    5757  λm, n: nat.
    5858  λb: BitVector n. pad_vector ? false m n b.
    59  
     59
     60(* jpb: we already have bitvector_of_nat and friends in the library, maybe
     61 * we should unify this in some way *) 
    6062let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
    6163  match n with
Note: See TracChangeset for help on using the changeset viewer.