package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Arm_extra

type __ = Obj.t
type arm_extra_op =
  1. | Oarm_swap of Wsize.wsize
  2. | Oarm_add_large_imm
  3. | Osmart_li of Wsize.wsize
  4. | Osmart_li_cc of Wsize.wsize
val arm_extra_op_rect : (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> arm_extra_op -> 'a1
val arm_extra_op_rec : (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> arm_extra_op -> 'a1
type is_arm_extra_op =
  1. | Coq_is_Oarm_swap of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_Oarm_add_large_imm
  3. | Coq_is_Osmart_li of Wsize.wsize * Wsize.is_wsize
  4. | Coq_is_Osmart_li_cc of Wsize.wsize * Wsize.is_wsize
val is_arm_extra_op_rect : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> arm_extra_op -> is_arm_extra_op -> 'a1
val is_arm_extra_op_rec : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> arm_extra_op -> is_arm_extra_op -> 'a1
val arm_extra_op_tag : arm_extra_op -> BinNums.positive
val is_arm_extra_op_inhab : arm_extra_op -> is_arm_extra_op
val is_arm_extra_op_functor : arm_extra_op -> is_arm_extra_op -> is_arm_extra_op
type box_arm_extra_op_Oarm_swap = Wsize.wsize
val coq_Box_arm_extra_op_Oarm_swap_0 : box_arm_extra_op_Oarm_swap -> Wsize.wsize
type box_arm_extra_op_Oarm_add_large_imm =
  1. | Box_arm_extra_op_Oarm_add_large_imm
type arm_extra_op_fields_t = __
val arm_extra_op_fields : arm_extra_op -> arm_extra_op_fields_t
val arm_extra_op_construct : BinNums.positive -> arm_extra_op_fields_t -> arm_extra_op option
val arm_extra_op_induction : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> arm_extra_op -> is_arm_extra_op -> 'a1
val arm_extra_op_eqb_fields : (arm_extra_op -> arm_extra_op -> bool) -> BinNums.positive -> arm_extra_op_fields_t -> arm_extra_op_fields_t -> bool
val arm_extra_op_eqb : arm_extra_op -> arm_extra_op -> bool
val arm_extra_op_eqb_OK : arm_extra_op -> arm_extra_op -> Bool.reflect
val arm_extra_op_eqb_OK_sumbool : arm_extra_op -> arm_extra_op -> bool
val coq_HB_unnamed_factory_1 : arm_extra_op Eqtype.Coq_hasDecEq.axioms_
val arm_extra_arm_extra_op__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val eqTC_arm_extra_op : arm_extra_op Utils0.eqTypeC
val coq_Oarm_add_large_imm_instr : Sopn.instruction_desc
val smart_li_instr : Wsize.wsize -> Sopn.instruction_desc
val smart_li_instr_cc : Wsize.wsize -> Sopn.instruction_desc
val get_instr_desc : arm_extra_op -> Sopn.instruction_desc
val arm_extra_op_decl : arm_extra_op Sopn.asmOp
module E : sig ... end
val uncons : Expr.instr_info -> 'a1 list -> ('a1 * 'a1 list) Compiler_util.cexec