package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Inductive and coinductive types

Entry points for the vernacular commands Inductive and CoInductive

type uniform_inductive_flag =
  1. | UniformParameters
  2. | NonUniformParameters
val do_mutual_inductive : template:bool option -> Constrexpr.cumul_univ_decl_expr option -> (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list -> cumulative:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> private_ind:bool -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> unit

User-interface API

Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables. Not_found is raised if the given string isn't the qualid of a known inductive type.

val make_cases : Names.inductive -> string list list
module Mind_decl : sig ... end
val interp_mutual_inductive : env:Environ.env -> template:bool option -> Constrexpr.cumul_univ_decl_expr option -> (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list -> cumulative:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> private_ind:bool -> uniform:uniform_inductive_flag -> Declarations.recursivity_kind -> Mind_decl.t

elaborates an inductive declaration (the first half of do_mutual_inductive)

val interp_mutual_inductive_constr : sigma:Evd.evar_map -> template:bool option -> udecl:UState.universe_decl -> variances:Entries.variance_entry -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> indnames:Names.Id.t list -> arities:EConstr.t list -> arityconcl:EConstr.ESorts.t option list -> constructors:(Names.Id.t list * EConstr.constr list) list -> env_ar_params:Environ.env -> cumulative:bool -> poly:bool -> private_ind:bool -> finite:Declarations.recursivity_kind -> Entries.mutual_inductive_entry * UnivNames.universe_binders * Univ.ContextSet.t

the post-elaboration part of interp_mutual_inductive, mainly dealing with universe levels

Internal API, exported for Record

val compute_template_inductive : user_template:bool option -> env_ar_params:Environ.env -> ctx_params:(Constr.constr, Constr.constr) Context.Rel.Declaration.pt list -> univ_entry:UState.universes_entry -> Entries.one_inductive_entry -> Sorts.t option -> Entries.inductive_universes_entry * Univ.ContextSet.t

compute_template_inductive computes whether an inductive can be template polymorphic.

val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int -> EConstr.t -> Evd.evar_map

nparams is the number of parameters which aren't treated as uniform, ie the length of params (including letins) where the env is uniform params, inductives, params, binders.

val variance_of_entry : cumulative:bool -> variances:Entries.variance_entry -> Entries.inductive_universes_entry -> Entries.variance_entry option

Will return None if non-cumulative, and resize if there are more universes than originally specified. If monomorphic, cumulative is treated as false.

module Internal : sig ... end
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