package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception Elimconst
module ReductionBehaviour : sig ... end
type effect_name = string
val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
val set_reduction_effect : Names.Constant.t -> effect_name -> unit
val reduction_effect_hook : Environ.env -> Evd.evar_map -> Names.Constant.t -> Constr.constr Lazy.t -> unit
module Cst_stack : sig ... end
module Stack : sig ... end
type reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
type e_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
type contextual_stack_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function = Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
type state_reduction_function = Environ.env -> Evd.evar_map -> state -> state
type local_state_reduction_function = Evd.evar_map -> state -> state
val pr_state : Environ.env -> Evd.evar_map -> state -> Pp.t
val stacklam : (state -> 'a) -> EConstr.constr list -> Evd.evar_map -> EConstr.constr -> EConstr.constr Stack.t -> 'a
val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
val nf_beta : reduction_function
val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
val nf_zeta : reduction_function
val nf_all : reduction_function
val whd_nored : reduction_function
val whd_beta : reduction_function
val whd_betaiota : reduction_function
val whd_betaiotazeta : reduction_function
val whd_all : reduction_function
val whd_allnolet : reduction_function
val whd_betalet : reduction_function
val whd_betaiota_stack : contextual_stack_reduction_function
val whd_betaiotazeta_stack : contextual_stack_reduction_function
val whd_allnolet_stack : contextual_stack_reduction_function
val whd_betalet_stack : contextual_stack_reduction_function
val whd_nored_state : state_reduction_function
val whd_beta_state : state_reduction_function
val whd_betaiota_state : state_reduction_function
val whd_betaiotazeta_state : state_reduction_function
val whd_all_state : state_reduction_function
val whd_allnolet_state : state_reduction_function
val whd_betalet_state : state_reduction_function
val whd_delta_stack : stack_reduction_function
val whd_delta_state : state_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
val whd_betadeltazeta_state : state_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : stack_reduction_function
val whd_zeta_state : state_reduction_function
val whd_zeta : reduction_function
val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr option
val beta_applist : Evd.evar_map -> (EConstr.constr * EConstr.constr list) -> EConstr.constr
val hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
val hnf_prod_applist : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val hnf_lam_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
type !'a miota_args = {
  1. mP : EConstr.constr;
  2. mconstr : EConstr.constr;
  3. mci : Constr.case_info;
  4. mcargs : 'a list;
  5. mlf : 'a array;
}
val reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool
val is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val contract_fix : ?env:Environ.env -> Evd.evar_map -> ?reference:Names.Constant.t -> EConstr.fixpoint -> EConstr.constr
val fix_recarg : ('a, 'a) Constr.pfixpoint -> 'b Stack.t -> (int * 'b) option
val is_transparent : Environ.env -> Names.Constant.t Names.tableKey -> bool
type conversion_test = Univ.Constraint.t -> Univ.Constraint.t
val pb_is_equal : Evd.conv_pb -> bool
val pb_equal : Evd.conv_pb -> Evd.conv_pb
val is_conv_leq : ?reds:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val infer_conv : ?catch_incon:bool -> ?pb:Evd.conv_pb -> ?ts:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
val set_vm_infer_conv : (?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option) -> unit
val vm_infer_conv : ?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
val whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct