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/ltac2_plugin/Ltac2_plugin/Tac2print/index.html
Module Ltac2_plugin.Tac2print
Source
Prints the shortest name for the constant. Also works for constants not in the nametab (because they're local to another module).
Printing types
Printing expressions
Source
val pr_glbexpr_gen :
Tac2expr.exp_level ->
avoid:Names.Id.Set.t ->
Tac2expr.glb_tacexpr ->
Pp.t
Source
val pr_rawexpr_gen :
Tac2expr.exp_level ->
avoid:Names.Id.Set.t ->
Tac2expr.raw_tacexpr ->
Pp.t
Utility function
Printing values
Source
type val_printer = {
val_printer : 'a. Environ.env -> Evd.evar_map -> Tac2ffi.valexpr -> 'a Tac2expr.glb_typexpr list -> Pp.t;
}
Source
val pr_valexpr :
Environ.env ->
Evd.evar_map ->
Tac2ffi.valexpr ->
'a Tac2expr.glb_typexpr ->
Pp.t
Utilities
Create a function that give names to integers. The names are generated on the fly, in the order they are encountered.
Ltac2 primitives
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page