package coq

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

Module ReductionSource

Sourceval whd_betaiotazeta : Environ.env -> Constr.constr -> Constr.constr
Sourceexception NotConvertible
Sourcetype 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit
Sourcetype 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> Environ.env -> ?evars:(Constr.existential -> Constr.constr option) -> 'a -> 'a -> unit
Sourcetype conv_pb =
  1. | CONV
  2. | CUMUL
Sourcetype 'a universe_compare = {
  1. compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
  2. compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
  3. compare_cumul_instances : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}
Sourcetype 'a universe_state = 'a * 'a universe_compare
Sourcetype ('a, 'b) generic_conversion_function = Environ.env -> 'b universe_state -> 'a -> 'a -> 'b
Sourcetype 'a infer_conversion_function = Environ.env -> 'a -> 'a -> Univ.Constraints.t
Sourceval get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraints.t
Sourceval inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
Sourceval constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
Sourceval sort_cmp_universes : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
Sourceval convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> ('a * 'a universe_compare) -> 'a * 'a universe_compare
Sourceval checked_universes : UGraph.t universe_compare

These two never raise UnivInconsistency, inferred_universes just gathers the constraints.

These two functions can only raise NotConvertible

Sourceval infer_conv : ?l2r:bool -> ?evars:(Constr.existential -> Constr.constr option) -> ?ts:TransparentState.t -> Constr.constr infer_conversion_function

These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel

Sourceval infer_conv_leq : ?l2r:bool -> ?evars:(Constr.existential -> Constr.constr option) -> ?ts:TransparentState.t -> Constr.types infer_conversion_function

Depending on the universe state functions, this might raise UniverseInconsistency in addition to NotConvertible (for better error messages).

Sourceval beta_applist : Constr.constr -> Constr.constr list -> Constr.constr

Builds an application node, reducing beta redexes it may produce.

Sourceval beta_appvect : Constr.constr -> Constr.constr array -> Constr.constr

Builds an application node, reducing beta redexes it may produce.

Builds an application node, reducing beta redexe it may produce.

Sourceval hnf_prod_applist : Environ.env -> Constr.types -> Constr.constr list -> Constr.types

Pseudo-reduction rule Prod(x,A,B) a --> Bx\a

Sourceval hnf_prod_applist_assum : Environ.env -> int -> Constr.types -> Constr.constr list -> Constr.types

In hnf_prod_applist_assum n c args, c is supposed to (whd-)reduce to the form ∀Γ.t with Γ of length n and possibly with let-ins; it returns t with the assumptions of Γ instantiated by args and the local definitions of Γ expanded.

Sourceval betazeta_appvect : int -> Constr.constr -> Constr.constr array -> Constr.constr

Compatibility alias for Term.lambda_appvect_assum

Sourceexception NotArity
Sourceval is_arity : Environ.env -> Constr.types -> bool
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