sibylfs-lem 0.4.0 (latest)

type bitSequence =

| BitSeq of int option * bool * bool list

val instance_Basic_classes_Eq_Word_bitSequence_dict : 
  'a Lem_basic_classes.eq_class

val boolListFrombitSeqAux : Nat_num.nat -> 'a -> 'a list -> 'a list

val boolListFrombitSeq : Nat_num.nat -> bitSequence -> bool list

val bitSeqFromBoolList : bool list -> bitSequence option

val cleanBitSeq : bitSequence -> bitSequence

val bitSeqTestBit : bitSequence -> Nat_num.nat -> bool option

val bitSeqSetBit : bitSequence -> Nat_num.nat -> bool -> bitSequence

val resizeBitSeq : Nat_num.nat option -> bitSequence -> bitSequence

val bitSeqNot : bitSequence -> bitSequence

val bitSeqBinopAux : 
  ('a -> 'b -> 'c) ->
  'a ->
  'a list ->
  'b ->
  'b list ->
  'c list

val bitSeqBinop : 
  (bool -> bool -> bool) ->
  bitSequence ->
  bitSequence ->
  bitSequence

val bitSeqAnd : bitSequence -> bitSequence -> bitSequence

val bitSeqOr : bitSequence -> bitSequence -> bitSequence

val bitSeqXor : bitSequence -> bitSequence -> bitSequence

val bitSeqShiftLeft : bitSequence -> Nat_num.nat -> bitSequence

val bitSeqArithmeticShiftRight : bitSequence -> Nat_num.nat -> bitSequence

val bitSeqLogicalShiftRight : bitSequence -> Nat_num.nat -> bitSequence

val integerFromBoolListAux : Big_int.big_int -> bool list -> Big_int.big_int

val integerFromBoolList : (bool * bool list) -> Big_int.big_int

val boolListFromNatural : bool list -> Big_int.big_int -> bool list

val boolListFromInteger : Big_int.big_int -> bool * bool list

val bitSeqFromInteger : Nat_num.nat option -> Big_int.big_int -> bitSequence

val integerFromBitSeq : bitSequence -> Big_int.big_int

val bitSeqArithUnaryOp : 
  (Big_int.big_int -> Big_int.big_int) ->
  bitSequence ->
  bitSequence

val bitSeqArithBinOp : 
  (Big_int.big_int -> Big_int.big_int -> Big_int.big_int) ->
  bitSequence ->
  bitSequence ->
  bitSequence

val bitSeqArithBinTest : 
  (Big_int.big_int -> Big_int.big_int -> 'a) ->
  bitSequence ->
  bitSequence ->
  'a

val bitSeqLess : bitSequence -> bitSequence -> bool

val bitSeqLessEqual : bitSequence -> bitSequence -> bool

val bitSeqGreater : bitSequence -> bitSequence -> bool

val bitSeqGreaterEqual : bitSequence -> bitSequence -> bool

val bitSeqCompare : bitSequence -> bitSequence -> int

val instance_Basic_classes_Ord_Word_bitSequence_dict : 
  bitSequence Lem_basic_classes.ord_class

val instance_Basic_classes_SetType_Word_bitSequence_dict : 
  bitSequence Lem_basic_classes.setType_class

val bitSeqNegate : bitSequence -> bitSequence

val instance_Num_NumNegate_Word_bitSequence_dict : 
  bitSequence Lem_num.numNegate_class

val bitSeqAdd : bitSequence -> bitSequence -> bitSequence

val instance_Num_NumAdd_Word_bitSequence_dict : 
  bitSequence Lem_num.numAdd_class

val bitSeqMinus : bitSequence -> bitSequence -> bitSequence

val instance_Num_NumMinus_Word_bitSequence_dict : 
  bitSequence Lem_num.numMinus_class

val bitSeqSucc : bitSequence -> bitSequence

val instance_Num_NumSucc_Word_bitSequence_dict : 
  bitSequence Lem_num.numSucc_class

val bitSeqPred : bitSequence -> bitSequence

val instance_Num_NumPred_Word_bitSequence_dict : 
  bitSequence Lem_num.numPred_class

val bitSeqMult : bitSequence -> bitSequence -> bitSequence

val instance_Num_NumMult_Word_bitSequence_dict : 
  bitSequence Lem_num.numMult_class

val bitSeqPow : bitSequence -> int -> bitSequence

val instance_Num_NumPow_Word_bitSequence_dict : 
  bitSequence Lem_num.numPow_class

val bitSeqDiv : bitSequence -> bitSequence -> bitSequence

val instance_Num_NumIntegerDivision_Word_bitSequence_dict : 
  bitSequence Lem_num.numIntegerDivision_class

val instance_Num_NumDivision_Word_bitSequence_dict : 
  bitSequence Lem_num.numDivision_class

val bitSeqMod : bitSequence -> bitSequence -> bitSequence

val instance_Num_NumRemainder_Word_bitSequence_dict : 
  bitSequence Lem_num.numRemainder_class

val bitSeqMin : bitSequence -> bitSequence -> bitSequence

val bitSeqMax : bitSequence -> bitSequence -> bitSequence

val instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict : 
  bitSequence Lem_basic_classes.ordMaxMin_class

type !'a wordNot_class = {

lnot_method : 'a -> 'a;

}

type !'a wordAnd_class = {

land_method : 'a -> 'a -> 'a;

}

type !'a wordOr_class = {

lor_method : 'a -> 'a -> 'a;

}

type !'a wordXor_class = {

lxor_method : 'a -> 'a -> 'a;

}

type !'a wordLsl_class = {

lsl_method : 'a -> int -> 'a;

}

type !'a wordLsr_class = {

lsr_method : 'a -> int -> 'a;

}

type !'a wordAsr_class = {

asr_method : 'a -> int -> 'a;

}

val instance_Word_WordNot_Word_bitSequence_dict : bitSequence wordNot_class

val instance_Word_WordAnd_Word_bitSequence_dict : bitSequence wordAnd_class

val instance_Word_WordOr_Word_bitSequence_dict : bitSequence wordOr_class

val instance_Word_WordXor_Word_bitSequence_dict : bitSequence wordXor_class

val instance_Word_WordLsl_Word_bitSequence_dict : bitSequence wordLsl_class

val instance_Word_WordLsr_Word_bitSequence_dict : bitSequence wordLsr_class

val instance_Word_WordAsr_Word_bitSequence_dict : bitSequence wordAsr_class

val instance_Word_WordNot_Num_int32_dict : int32 wordNot_class

val instance_Word_WordOr_Num_int32_dict : int32 wordOr_class

val instance_Word_WordXor_Num_int32_dict : int32 wordXor_class

val instance_Word_WordAnd_Num_int32_dict : int32 wordAnd_class

val instance_Word_WordLsl_Num_int32_dict : int32 wordLsl_class

val instance_Word_WordLsr_Num_int32_dict : int32 wordLsr_class

val instance_Word_WordAsr_Num_int32_dict : int32 wordAsr_class

val instance_Word_WordNot_Num_int64_dict : int64 wordNot_class

val instance_Word_WordOr_Num_int64_dict : int64 wordOr_class

val instance_Word_WordXor_Num_int64_dict : int64 wordXor_class

val instance_Word_WordAnd_Num_int64_dict : int64 wordAnd_class

val instance_Word_WordLsl_Num_int64_dict : int64 wordLsl_class

val instance_Word_WordLsr_Num_int64_dict : int64 wordLsr_class

val instance_Word_WordAsr_Num_int64_dict : int64 wordAsr_class

val defaultLnot : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'a

val defaultLand : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'b -> 'a

val defaultLor : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'b -> 'a

val defaultLxor : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'b -> 'a

val defaultLsl : 
  (bitSequence -> 'a) ->
  ('b -> bitSequence) ->
  'b ->
  Nat_num.nat ->
  'a

val defaultLsr : 
  (bitSequence -> 'a) ->
  ('b -> bitSequence) ->
  'b ->
  Nat_num.nat ->
  'a

val defaultAsr : 
  (bitSequence -> 'a) ->
  ('b -> bitSequence) ->
  'b ->
  Nat_num.nat ->
  'a

val integerLnot : Big_int.big_int -> Big_int.big_int

val instance_Word_WordNot_Num_integer_dict : Big_int.big_int wordNot_class

val instance_Word_WordOr_Num_integer_dict : Big_int.big_int wordOr_class

val instance_Word_WordXor_Num_integer_dict : Big_int.big_int wordXor_class

val instance_Word_WordAnd_Num_integer_dict : Big_int.big_int wordAnd_class

val instance_Word_WordLsl_Num_integer_dict : Big_int.big_int wordLsl_class

val instance_Word_WordLsr_Num_integer_dict : Big_int.big_int wordLsr_class

val instance_Word_WordAsr_Num_integer_dict : Big_int.big_int wordAsr_class

val intFromBitSeq : bitSequence -> int

val bitSeqFromInt : int -> bitSequence

val instance_Word_WordNot_Num_int_dict : int wordNot_class

val instance_Word_WordOr_Num_int_dict : int wordOr_class

val instance_Word_WordXor_Num_int_dict : int wordXor_class

val instance_Word_WordAnd_Num_int_dict : int wordAnd_class

val instance_Word_WordLsl_Num_int_dict : int wordLsl_class

val instance_Word_WordAsr_Num_int_dict : int wordAsr_class

val naturalFromBitSeq : bitSequence -> Big_int.big_int

val bitSeqFromNatural : Nat_num.nat option -> Big_int.big_int -> bitSequence

val instance_Word_WordOr_Num_natural_dict : Big_int.big_int wordOr_class

val instance_Word_WordXor_Num_natural_dict : Big_int.big_int wordXor_class

val instance_Word_WordAnd_Num_natural_dict : Big_int.big_int wordAnd_class

val instance_Word_WordLsl_Num_natural_dict : Big_int.big_int wordLsl_class

val instance_Word_WordLsr_Num_natural_dict : Big_int.big_int wordLsr_class

val instance_Word_WordAsr_Num_natural_dict : Big_int.big_int wordAsr_class

val natFromBitSeq : bitSequence -> int

val bitSeqFromNat : int -> bitSequence

val instance_Word_WordOr_nat_dict : int wordOr_class

val instance_Word_WordXor_nat_dict : int wordXor_class

val instance_Word_WordAnd_nat_dict : int wordAnd_class

val instance_Word_WordLsl_nat_dict : int wordLsl_class

val instance_Word_WordAsr_nat_dict : int wordAsr_class

package sibylfs-lem