package jasmin

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

Module Jasmin.Riscv_extra

type __ = Obj.t
type riscv_extra_op =
  1. | SWAP of Wsize.wsize
  2. | Oriscv_add_large_imm
val riscv_extra_op_rect : (Wsize.wsize -> 'a1) -> 'a1 -> riscv_extra_op -> 'a1
val riscv_extra_op_rec : (Wsize.wsize -> 'a1) -> 'a1 -> riscv_extra_op -> 'a1
type is_riscv_extra_op =
  1. | Coq_is_SWAP of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_Oriscv_add_large_imm
val is_riscv_extra_op_rect : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> riscv_extra_op -> is_riscv_extra_op -> 'a1
val is_riscv_extra_op_rec : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> riscv_extra_op -> is_riscv_extra_op -> 'a1
val riscv_extra_op_tag : riscv_extra_op -> BinNums.positive
val is_riscv_extra_op_inhab : riscv_extra_op -> is_riscv_extra_op
val is_riscv_extra_op_functor : riscv_extra_op -> is_riscv_extra_op -> is_riscv_extra_op
type box_riscv_extra_op_SWAP = Wsize.wsize
val coq_Box_riscv_extra_op_SWAP_0 : box_riscv_extra_op_SWAP -> Wsize.wsize
type box_riscv_extra_op_Oriscv_add_large_imm =
  1. | Box_riscv_extra_op_Oriscv_add_large_imm
type riscv_extra_op_fields_t = __
val riscv_extra_op_fields : riscv_extra_op -> riscv_extra_op_fields_t
val riscv_extra_op_construct : BinNums.positive -> riscv_extra_op_fields_t -> riscv_extra_op option
val riscv_extra_op_induction : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> riscv_extra_op -> is_riscv_extra_op -> 'a1
val riscv_extra_op_eqb_fields : (riscv_extra_op -> riscv_extra_op -> bool) -> BinNums.positive -> riscv_extra_op_fields_t -> riscv_extra_op_fields_t -> bool
val riscv_extra_op_eqb : riscv_extra_op -> riscv_extra_op -> bool
val riscv_extra_op_eqb_OK : riscv_extra_op -> riscv_extra_op -> Bool.reflect
val riscv_extra_op_eqb_OK_sumbool : riscv_extra_op -> riscv_extra_op -> bool
val coq_HB_unnamed_factory_1 : riscv_extra_op Eqtype.Coq_hasDecEq.axioms_
val riscv_extra_riscv_extra_op__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val eqTC_riscv_extra_op : riscv_extra_op Utils0.eqTypeC
val coq_Oriscv_add_large_imm_instr : Sopn.instruction_desc
val get_instr_desc : riscv_extra_op -> Sopn.instruction_desc
val riscv_extra_op_decl : riscv_extra_op Sopn.asmOp
module E : sig ... end