Module `Reduction`Source

Sourceval whd_betaiotazeta : Environ.env -> Constr.constr -> Constr.constr

Sourceval whd_all : Environ.env -> Constr.constr -> Constr.constr

Sourceval whd_allnolet : Environ.env -> Constr.constr -> Constr.constr

Sourceval whd_betaiota : Environ.env -> Constr.constr -> Constr.constr

Sourceval nf_betaiota : Environ.env -> Constr.constr -> Constr.constr

Sourceexception NotConvertible

Sourcetype 'a kernel_conversion_function = Environ.env -> 'a -> 'a -> unit

type 'a extended_conversion_function =
  ?l2r:bool ->
  ?reds:TransparentState.t ->
  Environ.env ->
  ?evars:(Constr.existential -> Constr.constr option) ->
  'a ->
  'a ->
  unit

Sourcetype conv_pb =

| CONV
| CUMUL

Sourcetype 'a universe_compare = {

compare_sorts : Environ.env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
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

Source

type ('a, 'b) generic_conversion_function =
  Environ.env ->
  'b universe_state ->
  'a ->
  'a ->
  'b

Source

type 'a infer_conversion_function =
  Environ.env ->
  'a ->
  'a ->
  Univ.Constraint.t

Source

val get_cumulativity_constraints : 
  conv_pb ->
  Univ.Variance.t array ->
  Univ.Instance.t ->
  Univ.Instance.t ->
  Univ.Constraint.t

Source

val inductive_cumulativity_arguments : 
  (Declarations.mutual_inductive_body * int) ->
  int

Source

val constructor_cumulativity_arguments : 
  (Declarations.mutual_inductive_body * int * int) ->
  int

Source

val sort_cmp_universes : 
  Environ.env ->
  conv_pb ->
  Sorts.t ->
  Sorts.t ->
  ('a * 'a universe_compare) ->
  'a * 'a universe_compare

Source

val 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.

Sourceval inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare

Sourceval conv : Constr.constr extended_conversion_function

These two functions can only raise NotConvertible

Sourceval conv_leq : Constr.types extended_conversion_function

Source

val 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

Source

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

Source

val generic_conv : 
  conv_pb ->
  l2r:bool ->
  (Constr.existential -> Constr.constr option) ->
  TransparentState.t ->
  (Constr.constr, 'a) generic_conversion_function

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

Source

val default_conv : 
  conv_pb ->
  ?l2r:bool ->
  Constr.types kernel_conversion_function

Sourceval default_conv_leq : ?l2r:bool -> Constr.types kernel_conversion_function

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.

Sourceval beta_app : Constr.constr -> Constr.constr -> Constr.constr

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

Source

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

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

Source

val 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.

Source

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

Compatibility alias for Term.lambda_appvect_assum

Source

val dest_prod : 
  Environ.env ->
  Constr.types ->
  Constr.rel_context * Constr.types

Source

val dest_prod_assum : 
  Environ.env ->
  Constr.types ->
  Constr.rel_context * Constr.types

Source

val dest_lam : 
  Environ.env ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

Source

val dest_lam_assum : 
  Environ.env ->
  Constr.constr ->
  Constr.rel_context * Constr.constr

Sourceexception NotArity

Sourceval dest_arity : Environ.env -> Constr.types -> Term.arity

Sourceval is_arity : Environ.env -> Constr.types -> bool

Sourceval eta_expand : Environ.env -> Constr.constr -> Constr.types -> Constr.constr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Reduction/index.html

Module `Reduction`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Reduction/index.html

Module ReductionSource

Module `Reduction`Source