package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/coq-core.vernac/Vernacentries/Preprocessed_Mind_decl/index.html
Module Vernacentries.Preprocessed_Mind_declSource
pre-processing and validation of VernacInductive
Source
type flags = {template : bool option;udecl : Constrexpr.cumul_univ_decl_expr option;cumulative : bool;poly : bool;finite : Declarations.recursivity_kind;
}Source
type record = {flags : flags;primitive_proj : bool;kind : Vernacexpr.inductive_kind;records : Record.Ast.t list;
}Source
type inductive = {flags : flags;typing_flags : Declarations.typing_flags option;private_ind : bool;uniform : ComInductive.uniform_inductive_flag;inductives : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list;
}