package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
doc/coq-core.toplevel/Coqtop/index.html
Module Coqtop
Source
Definition of custom toplevels. init_extra
is used to do custom initialization run
launches a custom toplevel.
Source
type ('a, 'b) custom_toplevel = {
parse_extra : string list -> 'a * string list;
usage : Boot.Usage.specific_usage;
init_extra : 'a -> Coqargs.injection_command list -> opts:Coqargs.t -> 'b;
initial_args : Coqargs.t;
run : 'a -> opts:Coqargs.t -> 'b -> unit;
}
The generic Coq main module. start custom
will parse the command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch custom.run
.
Prepare state for interactive loop
Source
val init_toploop :
Coqargs.t ->
Stm.AsyncOpts.stm_opt ->
Coqargs.injection_command list ->
Vernac.State.t
The specific characterization of the coqtop_toplevel
Source
val coqtop_toplevel :
(toplevel_options * Stm.AsyncOpts.stm_opt, Vernac.State.t) custom_toplevel
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>