package sibylfs-lem

  1. Overview
  2. Docs
type !'a eq_class = 'a Lem_basic_classes.eq_class = {
  1. isEqual_method : 'a -> 'a -> bool;
  2. isInequal_method : 'a -> 'a -> bool;
}
val unsafe_structural_inequality : 'a -> 'a -> bool
val instance_Basic_classes_Eq_var_dict : 'a eq_class
val instance_Basic_classes_Eq_Basic_classes_ordering_dict : int eq_class
type !'a ord_class = 'a Lem_basic_classes.ord_class = {
  1. compare_method : 'a -> 'a -> int;
  2. isLess_method : 'a -> 'a -> bool;
  3. isLessEqual_method : 'a -> 'a -> bool;
  4. isGreater_method : 'a -> 'a -> bool;
  5. isGreaterEqual_method : 'a -> 'a -> bool;
}
val genericCompare : ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> 'a -> 'a -> int
val ordCompare : 'a eq_class -> 'a ord_class -> 'a -> 'a -> int
type !'a ordMaxMin_class = 'a Lem_basic_classes.ordMaxMin_class = {
  1. max_method : 'a -> 'a -> 'a;
  2. min_method : 'a -> 'a -> 'a;
}
val minByLessEqual : ('a -> 'a -> bool) -> 'a -> 'a -> 'a
val maxByLessEqual : ('a -> 'a -> bool) -> 'a -> 'a -> 'a
val instance_Basic_classes_OrdMaxMin_var_dict : 'a -> 'b ordMaxMin_class
type !'a setType_class = 'a Lem_basic_classes.setType_class = {
  1. setElemCompare_method : 'a -> 'a -> int;
}
val instance_Basic_classes_SetType_var_dict : 'a setType_class
val instance_Basic_classes_Eq_bool_dict : 'a eq_class
val boolCompare : bool -> bool -> int
val instance_Basic_classes_SetType_bool_dict : bool setType_class
val instance_Basic_classes_Eq_char_dict : 'a eq_class
val instance_Basic_classes_Eq_string_dict : 'a eq_class
val instance_Basic_classes_Eq_tup2_dict : 'a eq_class -> 'b eq_class -> ('a * 'b) eq_class
val pairCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('a * 'c) -> ('b * 'd) -> int
val pairLess : 'a ord_class -> 'b ord_class -> ('b * 'a) -> ('b * 'a) -> bool
val pairLessEq : 'a ord_class -> 'b ord_class -> ('b * 'a) -> ('b * 'a) -> bool
val pairGreater : 'a ord_class -> 'b ord_class -> ('a * 'b) -> ('a * 'b) -> bool
val pairGreaterEq : 'a ord_class -> 'b ord_class -> ('a * 'b) -> ('a * 'b) -> bool
val instance_Basic_classes_Ord_tup2_dict : 'a ord_class -> 'b ord_class -> ('a * 'b) ord_class
val instance_Basic_classes_SetType_tup2_dict : 'a setType_class -> 'b setType_class -> ('a * 'b) setType_class
val tripleEqual : 'a eq_class -> 'b eq_class -> 'c eq_class -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool
val instance_Basic_classes_Eq_tup3_dict : 'a eq_class -> 'b eq_class -> 'c eq_class -> ('a * 'b * 'c) eq_class
val tripleCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('e -> 'f -> int) -> ('a * 'c * 'e) -> ('b * 'd * 'f) -> int
val tripleLess : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool
val tripleLessEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool
val tripleGreater : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('c * 'b * 'a) -> ('c * 'b * 'a) -> bool
val tripleGreaterEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('c * 'b * 'a) -> ('c * 'b * 'a) -> bool
val instance_Basic_classes_Ord_tup3_dict : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('a * 'b * 'c) ord_class
val instance_Basic_classes_SetType_tup3_dict : 'a setType_class -> 'b setType_class -> 'c setType_class -> ('a * 'b * 'c) setType_class
val instance_Basic_classes_Eq_Maybe_maybe_dict : 'a Lem_basic_classes.eq_class -> 'a option Lem_basic_classes.eq_class
val maybeCompare : ('a -> 'b -> int) -> 'a option -> 'b option -> int
val instance_Basic_classes_SetType_Maybe_maybe_dict : 'a Lem_basic_classes.setType_class -> 'a option Lem_basic_classes.setType_class
val instance_Basic_classes_Eq_Either_either_dict : 'a Lem_basic_classes.eq_class -> 'b Lem_basic_classes.eq_class -> ('a, 'b) Either.either Lem_basic_classes.eq_class
val id : 'a -> 'a
val comb : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val curry : (('a * 'b) -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> ('a * 'b) -> 'c
type !'a numNegate_class = 'a Lem_num.numNegate_class = {
  1. numNegate_method : 'a -> 'a;
}
type !'a numAbs_class = 'a Lem_num.numAbs_class = {
  1. abs_method : 'a -> 'a;
}
type !'a numAdd_class = 'a Lem_num.numAdd_class = {
  1. numAdd_method : 'a -> 'a -> 'a;
}
type !'a numMinus_class = 'a Lem_num.numMinus_class = {
  1. numMinus_method : 'a -> 'a -> 'a;
}
type !'a numMult_class = 'a Lem_num.numMult_class = {
  1. numMult_method : 'a -> 'a -> 'a;
}
type !'a numPow_class = 'a Lem_num.numPow_class = {
  1. numPow_method : 'a -> int -> 'a;
}
type !'a numDivision_class = 'a Lem_num.numDivision_class = {
  1. numDivision_method : 'a -> 'a -> 'a;
}
type !'a numIntegerDivision_class = 'a Lem_num.numIntegerDivision_class = {
  1. div_method : 'a -> 'a -> 'a;
}
type !'a numRemainder_class = 'a Lem_num.numRemainder_class = {
  1. mod_method : 'a -> 'a -> 'a;
}
type !'a numSucc_class = 'a Lem_num.numSucc_class = {
  1. succ_method : 'a -> 'a;
}
type !'a numPred_class = 'a Lem_num.numPred_class = {
  1. pred_method : 'a -> 'a;
}
val instance_Basic_classes_Eq_nat_dict : 'a Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_nat_dict : 'a Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_nat_dict : 'a Lem_basic_classes.setType_class
val instance_Num_NumAdd_nat_dict : int numAdd_class
val instance_Num_NumMinus_nat_dict : Nat_num.nat numMinus_class
val instance_Num_NumSucc_nat_dict : int numSucc_class
val instance_Num_NumPred_nat_dict : Nat_num.nat numPred_class
val instance_Num_NumMult_nat_dict : int numMult_class
val instance_Num_NumIntegerDivision_nat_dict : int numIntegerDivision_class
val instance_Num_NumDivision_nat_dict : int numDivision_class
val instance_Num_NumRemainder_nat_dict : int numRemainder_class
val gen_pow_aux : ('a -> 'a -> 'a) -> 'a -> 'a -> int -> 'a
val gen_pow : 'a -> ('a -> 'a -> 'a) -> 'a -> int -> 'a
val natPow : int -> int -> int
val instance_Num_NumPow_nat_dict : int numPow_class
val instance_Basic_classes_OrdMaxMin_nat_dict : 'a Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_natural_dict : Big_int.big_int Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_natural_dict : Big_int.big_int Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_natural_dict : Big_int.big_int Lem_basic_classes.setType_class
val instance_Num_NumAdd_Num_natural_dict : Big_int.big_int numAdd_class
val instance_Num_NumMinus_Num_natural_dict : Nat_num.natural numMinus_class
val instance_Num_NumSucc_Num_natural_dict : Big_int.big_int numSucc_class
val instance_Num_NumPred_Num_natural_dict : Nat_num.natural numPred_class
val instance_Num_NumMult_Num_natural_dict : Big_int.big_int numMult_class
val instance_Num_NumPow_Num_natural_dict : Big_int.big_int numPow_class
val instance_Num_NumIntegerDivision_Num_natural_dict : Big_int.big_int numIntegerDivision_class
val instance_Num_NumDivision_Num_natural_dict : Big_int.big_int numDivision_class
val instance_Num_NumRemainder_Num_natural_dict : Big_int.big_int numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_natural_dict : Big_int.big_int Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_int_dict : 'a Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_int_dict : 'a Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_int_dict : 'a Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_int_dict : int numNegate_class
val instance_Num_NumAbs_Num_int_dict : int numAbs_class
val instance_Num_NumAdd_Num_int_dict : int numAdd_class
val instance_Num_NumMinus_Num_int_dict : int numMinus_class
val instance_Num_NumSucc_Num_int_dict : int numSucc_class
val instance_Num_NumPred_Num_int_dict : int numPred_class
val instance_Num_NumMult_Num_int_dict : int numMult_class
val intPow : int -> int -> int
val instance_Num_NumPow_Num_int_dict : int numPow_class
val instance_Num_NumIntegerDivision_Num_int_dict : int numIntegerDivision_class
val instance_Num_NumDivision_Num_int_dict : int numDivision_class
val instance_Num_NumRemainder_Num_int_dict : int numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_int_dict : 'a Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_int32_dict : 'a Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_int32_dict : Int32.t Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_int32_dict : Int32.t Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_int32_dict : int32 numNegate_class
val instance_Num_NumAbs_Num_int32_dict : int32 numAbs_class
val instance_Num_NumAdd_Num_int32_dict : int32 numAdd_class
val instance_Num_NumMinus_Num_int32_dict : int32 numMinus_class
val instance_Num_NumSucc_Num_int32_dict : int32 numSucc_class
val instance_Num_NumPred_Num_int32_dict : int32 numPred_class
val instance_Num_NumMult_Num_int32_dict : int32 numMult_class
val int32Pow : int32 -> int -> int32
val instance_Num_NumPow_Num_int32_dict : int32 numPow_class
val instance_Num_NumIntegerDivision_Num_int32_dict : Int32.t numIntegerDivision_class
val instance_Num_NumDivision_Num_int32_dict : Int32.t numDivision_class
val instance_Num_NumRemainder_Num_int32_dict : Int32.t numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_int32_dict : 'a Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_int64_dict : 'a Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_int64_dict : Int64.t Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_int64_dict : Int64.t Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_int64_dict : int64 numNegate_class
val instance_Num_NumAbs_Num_int64_dict : int64 numAbs_class
val instance_Num_NumAdd_Num_int64_dict : int64 numAdd_class
val instance_Num_NumMinus_Num_int64_dict : int64 numMinus_class
val instance_Num_NumSucc_Num_int64_dict : int64 numSucc_class
val instance_Num_NumPred_Num_int64_dict : int64 numPred_class
val instance_Num_NumMult_Num_int64_dict : int64 numMult_class
val int64Pow : int64 -> int -> int64
val instance_Num_NumPow_Num_int64_dict : int64 numPow_class
val instance_Num_NumIntegerDivision_Num_int64_dict : Int64.t numIntegerDivision_class
val instance_Num_NumDivision_Num_int64_dict : Int64.t numDivision_class
val instance_Num_NumRemainder_Num_int64_dict : Int64.t numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_int64_dict : 'a Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_integer_dict : Big_int.big_int Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_integer_dict : Big_int.big_int Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_integer_dict : Big_int.big_int Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_integer_dict : Big_int.big_int numNegate_class
val instance_Num_NumAbs_Num_integer_dict : Big_int.big_int numAbs_class
val instance_Num_NumAdd_Num_integer_dict : Big_int.big_int numAdd_class
val instance_Num_NumMinus_Num_integer_dict : Big_int.big_int numMinus_class
val instance_Num_NumSucc_Num_integer_dict : Big_int.big_int numSucc_class
val instance_Num_NumPred_Num_integer_dict : Big_int.big_int numPred_class
val instance_Num_NumMult_Num_integer_dict : Big_int.big_int numMult_class
val instance_Num_NumPow_Num_integer_dict : Big_int.big_int numPow_class
val instance_Num_NumIntegerDivision_Num_integer_dict : Big_int.big_int numIntegerDivision_class
val instance_Num_NumDivision_Num_integer_dict : Big_int.big_int numDivision_class
val instance_Num_NumRemainder_Num_integer_dict : Big_int.big_int numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_integer_dict : Big_int.big_int Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Map_map_dict : 'a -> 'b Lem_basic_classes.eq_class -> ('c, 'b) Pmap.map Lem_basic_classes.eq_class
type !'a mapKeyType_class = 'a Lem_map.mapKeyType_class = {
  1. mapKeyCompare_method : 'a -> 'a -> int;
}
val instance_Map_MapKeyType_var_dict : 'a Lem_basic_classes.setType_class -> 'a mapKeyType_class
val fromList : 'a mapKeyType_class -> ('a * 'b) list -> ('a, 'b) Pmap.map
val instance_Basic_classes_Eq_set_dict : 'a -> 'b Pset.set Lem_basic_classes.eq_class
val instance_Basic_classes_SetType_set_dict : 'a -> 'b Pset.set Lem_basic_classes.setType_class
val partition : 'a -> ('b -> bool) -> 'b Pset.set -> 'b Pset.set * 'b Pset.set
val split : 'a -> 'b Lem_basic_classes.ord_class -> 'b -> 'b Pset.set -> 'b Pset.set * 'b Pset.set
val splitMember : 'a -> 'b Lem_basic_classes.ord_class -> 'b -> 'b Pset.set -> 'b Pset.set * bool * 'b Pset.set
val leastFixedPoint : 'a -> Nat_num.nat -> ('b Pset.set -> 'b Pset.set) -> 'b Pset.set -> 'b Pset.set
val list_null : 'a list -> bool
val listEqualBy : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val instance_Basic_classes_Eq_list_dict : 'a Lem_basic_classes.eq_class -> 'a list Lem_basic_classes.eq_class
val lexicographic_compare : ('a -> 'b -> int) -> 'a list -> 'b list -> int
val lexicographic_less : ('a -> 'b -> bool) -> ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val lexicographic_less_eq : ('a -> 'b -> bool) -> ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val instance_Basic_classes_Ord_list_dict : 'a Lem_basic_classes.ord_class -> 'a list Lem_basic_classes.ord_class
val snoc : 'a -> 'a list -> 'a list
val dest_init_aux : 'a list -> 'a -> 'a list -> 'a list * 'a
val dest_init : 'a list -> ('a list * 'a) option
val list_index : 'a list -> Nat_num.nat -> 'a option
val find_indices_aux : int -> ('a -> bool) -> 'a list -> int list
val find_indices : ('a -> bool) -> 'a list -> int list
val find_index : ('a -> bool) -> 'a list -> int option
val genlist : (Nat_num.nat -> 'a) -> Nat_num.nat -> 'a list
val replicate : Nat_num.nat -> 'a -> 'a list
val split_at : Nat_num.nat -> 'a list -> 'a list * 'a list
val take : Nat_num.nat -> 'a list -> 'a list
val drop : Nat_num.nat -> 'a list -> 'a list
val dropWhile : ('a -> bool) -> 'a list -> 'a list
val takeWhile : ('a -> bool) -> 'a list -> 'a list
val isPrefixOf : 'a Lem_basic_classes.eq_class -> 'a list -> 'a list -> bool
val list_update : 'a list -> Nat_num.nat -> 'a -> 'a list
val elemBy : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
val list_find_opt : ('a -> bool) -> 'a list -> 'a option
val lookupBy : ('a -> 'b -> bool) -> 'a -> ('b * 'c) list -> 'c option
val reversePartition : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_delete_first : ('a -> bool) -> 'a list -> 'a list option
val list_delete : ('a -> 'b -> bool) -> 'a -> 'b list -> 'b list
val list_combine : 'a list -> 'b list -> ('a * 'b) list
val instance_Basic_classes_SetType_list_dict : 'a Lem_basic_classes.setType_class -> 'a list Lem_basic_classes.setType_class
val allDistinct : 'a -> 'b list -> bool
type bitSequence = Lem_word.bitSequence =
  1. | 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 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 = 'a Lem_word.wordNot_class = {
  1. lnot_method : 'a -> 'a;
}
type !'a wordAnd_class = 'a Lem_word.wordAnd_class = {
  1. land_method : 'a -> 'a -> 'a;
}
type !'a wordOr_class = 'a Lem_word.wordOr_class = {
  1. lor_method : 'a -> 'a -> 'a;
}
type !'a wordXor_class = 'a Lem_word.wordXor_class = {
  1. lxor_method : 'a -> 'a -> 'a;
}
type !'a wordLsl_class = 'a Lem_word.wordLsl_class = {
  1. lsl_method : 'a -> int -> 'a;
}
type !'a wordLsr_class = 'a Lem_word.wordLsr_class = {
  1. lsr_method : 'a -> int -> 'a;
}
type !'a wordAsr_class = 'a Lem_word.wordAsr_class = {
  1. 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
val fromJust : 'a option -> 'a
val leastFixedPointUnbounded : 'a -> ('b Pset.set -> 'b Pset.set) -> 'b Pset.set -> 'b Pset.set
val last : 'a list -> 'a
val init : 'a list -> 'a list
val foldl1 : ('a -> 'a -> 'a) -> 'a list -> 'a
val foldr1 : ('a -> 'a -> 'a) -> 'a list -> 'a
val findNonPure : ('a -> bool) -> 'a list -> 'a
type !'a show_class = 'a Lem_string_extra.show_class = {
  1. show_method : 'a -> string;
}
val natToStringHelper : int -> char list -> char list
val natToString : int -> string
val instance_String_extra_Show_nat_dict : int show_class
val naturalToStringHelper : Big_int.big_int -> char list -> char list
val naturalToString : Big_int.big_int -> string
val instance_String_extra_Show_Num_natural_dict : Big_int.big_int show_class
val stringLess : 'a -> 'a -> bool
val stringLessEq : 'a -> 'a -> bool
val stringGreater : 'a -> 'a -> bool
val stringGreaterEq : 'a -> 'a -> bool
val instance_Basic_classes_Ord_string_dict : 'a Lem_basic_classes.ord_class
val ensure : bool -> string -> unit