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 contextual_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
type reduction_function = contextual_reduction_function
type local_reduction_function = 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 contextual_state_reduction_function = Environ.env -> Evd.evar_map -> state -> state
type state_reduction_function = contextual_state_reduction_function
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_all : reduction_function
val whd_nored : local_reduction_function
val whd_betaiota : local_reduction_function
val whd_betaiotazeta : local_reduction_function
val whd_betalet : local_reduction_function
val whd_nored_stack : local_stack_reduction_function
val whd_beta_stack : local_stack_reduction_function
val whd_betaiota_stack : local_stack_reduction_function
val whd_betaiotazeta_stack : local_stack_reduction_function
val whd_allnolet_stack : contextual_stack_reduction_function
val whd_betalet_stack : local_stack_reduction_function
val whd_nored_state : local_state_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
val whd_betaiotazeta_state : local_state_reduction_function
val whd_allnolet_state : contextual_state_reduction_function
val whd_betalet_state : local_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 : local_stack_reduction_function
val whd_zeta_state : local_state_reduction_function
val shrink_eta : EConstr.constr -> EConstr.constr
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 infer_conv : ?catch_incon:bool -> ?pb:Evd.conv_pb -> ?ts:Names.transparent_state -> 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 head_unfold_under_prod : Names.transparent_state -> reduction_function
val betazetaevar_applist : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val whd_betaiota_deltazeta_for_iota_state : Names.transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> state * Cst_stack.t
val meta_reducible_instance : Evd.evar_map -> EConstr.constr Evd.freelisted -> EConstr.constr
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