Module Jasmin.Arm_common

type __ = Obj.t
type rflag =
  1. | NF
  2. | ZF
  3. | CF
  4. | VF
val rflag_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> 'a1
val rflag_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> 'a1
type is_rflag =
  1. | Coq_is_NF
  2. | Coq_is_ZF
  3. | Coq_is_CF
  4. | Coq_is_VF
val is_rflag_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val is_rflag_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val rflag_tag : rflag -> BinNums.positive
val is_rflag_inhab : rflag -> is_rflag
val is_rflag_functor : rflag -> is_rflag -> is_rflag
type box_rflag_NF =
  1. | Box_rflag_NF
type rflag_fields_t = __
val rflag_fields : rflag -> rflag_fields_t
val rflag_construct : BinNums.positive -> rflag_fields_t -> rflag option
val rflag_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val rflag_eqb_fields : (rflag -> rflag -> bool) -> BinNums.positive -> rflag_fields_t -> rflag_fields_t -> bool
val rflag_eqb : rflag -> rflag -> bool
val rflag_eqb_OK : rflag -> rflag -> Datatypes.reflect
val rflag_eqb_OK_sumbool : rflag -> rflag -> bool
val eqTC_rflag : rflag Utils0.eqTypeC
val rflag_eqType : Eqtype.Equality.coq_type
val rflags : rflag list
val finTC_rflag : rflag Utils0.finTypeC
val rflag_finType : Fintype.Finite.coq_type
val flag_to_string : rflag -> string
type condt =
  1. | EQ_ct
  2. | NE_ct
  3. | CS_ct
  4. | CC_ct
  5. | MI_ct
  6. | PL_ct
  7. | VS_ct
  8. | VC_ct
  9. | HI_ct
  10. | LS_ct
  11. | GE_ct
  12. | LT_ct
  13. | GT_ct
  14. | LE_ct
val condt_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> 'a1
val condt_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> 'a1
type is_condt =
  1. | Coq_is_EQ_ct
  2. | Coq_is_NE_ct
  3. | Coq_is_CS_ct
  4. | Coq_is_CC_ct
  5. | Coq_is_MI_ct
  6. | Coq_is_PL_ct
  7. | Coq_is_VS_ct
  8. | Coq_is_VC_ct
  9. | Coq_is_HI_ct
  10. | Coq_is_LS_ct
  11. | Coq_is_GE_ct
  12. | Coq_is_LT_ct
  13. | Coq_is_GT_ct
  14. | Coq_is_LE_ct
val is_condt_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val is_condt_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val condt_tag : condt -> BinNums.positive
val is_condt_inhab : condt -> is_condt
val is_condt_functor : condt -> is_condt -> is_condt
type box_condt_EQ_ct =
  1. | Box_condt_EQ_ct
type condt_fields_t = __
val condt_fields : condt -> condt_fields_t
val condt_construct : BinNums.positive -> condt_fields_t -> condt option
val condt_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val condt_eqb_fields : (condt -> condt -> bool) -> BinNums.positive -> condt_fields_t -> condt_fields_t -> bool
val condt_eqb : condt -> condt -> bool
val condt_eqb_OK : condt -> condt -> Datatypes.reflect
val condt_eqb_OK_sumbool : condt -> condt -> bool
val eqTC_condt : condt Utils0.eqTypeC
val condt_eqType : Eqtype.Equality.coq_type
val condts : condt list
val finTC_condt : condt Utils0.finTypeC
val condt_finType : Fintype.Finite.coq_type
val string_of_condt : condt -> string
val arm_eval_cond : (rflag -> (Utils0.error, bool) Utils0.result) -> condt -> (Utils0.error, bool) Utils0.result
val coq_Z_mod_lnot : BinNums.coq_Z -> Wsize.wsize -> BinNums.coq_Z