package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.interp/Modintern/index.html
Module Modintern
Source
Module internalization errors
Source
type module_internalization_error =
| NotAModuleNorModtype of Libnames.qualid
| NotAModuleType of Libnames.qualid
| NotAModule of Libnames.qualid
| IncorrectWithInModule
| IncorrectModuleApplication
Module expressions and module types are interpreted relatively to possible functor or functor signature arguments. When the input kind is ModAny (i.e. module or module type), we tries to interprete this ast as a module, and in case of failure, as a module type. The returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny.
Source
type module_struct_expr =
(Constrexpr.universe_decl_expr option * Constrexpr.constr_expr)
Declarations.module_alg_expr
Source
val intern_module_ast :
module_kind ->
Constrexpr.module_ast ->
module_struct_expr * Names.ModPath.t * module_kind
Module internalization, i.e. from AST to module expression
Source
val interp_module_ast :
Environ.env ->
module_kind ->
Names.ModPath.t ->
module_struct_expr ->
Entries.module_struct_entry * Univ.ContextSet.t
Module interpretation, i.e. from module expression to typed module entry
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>