package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.vernac/ComInductive/index.html

Module ComInductiveSource

Inductive and coinductive types

Entry points for the vernacular commands Inductive and CoInductive

Sourcetype uniform_inductive_flag =
  1. | UniformParameters
  2. | NonUniformParameters
Sourceval 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.

Sourceval make_cases : Names.inductive -> string list list
Sourcemodule Mind_decl : sig ... end
Sourceval 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)

Sourcetype syntax_allows_template_poly =
  1. | SyntaxAllowsTemplatePoly
  2. | SyntaxNoTemplatePoly
Sourceval interp_mutual_inductive_constr : sigma:Evd.evar_map -> template:bool option -> udecl:UState.universe_decl -> variances:Entries.variance_entry -> ctx_params:EConstr.rel_context -> indnames:Names.Id.t list -> arities_explicit:bool list -> arities:EConstr.t list -> template_syntax:syntax_allows_template_poly 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 -> DeclareInd.default_dep_elim list * 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

Sourceval compute_template_inductive : user_template:bool option -> ctx_params:Constr.rel_context -> univ_entry:UState.universes_entry -> Entries.one_inductive_entry -> syntax_allows_template_poly -> Entries.inductive_universes_entry * Univ.ContextSet.t

compute_template_inductive computes whether an inductive can be template polymorphic.

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

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

Sourcemodule Internal : sig ... end