package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.15.0.0.15.4.tbz
sha256=cffb0eacd9d155434f7cf384418c78a9d1cf189b65b080a456f50d9d3c3dcf5c
sha512=77eada7c9f2979ee8b00704ed49e65f6e0aadb1a24b73bb89581bf624f330d141340e0dfecd8b1517a11b2a9d823d8f84fcbdea419cc99536557019c5951b80e
doc/coq-serapi.serlib/Serlib/Ser_nativevalues/index.html
Module Serlib.Ser_nativevalues
Source
Source
type annot_sw = Nativevalues.annot_sw = {
asw_ind : Names.inductive;
asw_ci : Constr.case_info;
asw_reloc : reloc_table;
asw_finite : bool;
asw_prefix : string;
}
Source
type symbol = Nativevalues.symbol =
| SymbValue of t
| SymbSort of Sorts.t
| SymbName of Names.Name.t
| SymbConst of Names.Constant.t
| SymbMatch of annot_sw
| SymbInd of Names.inductive
| SymbMeta of Constr.metavariable
| SymbEvar of Evar.t
| SymbLevel of Univ.Level.t
| SymbProj of Names.inductive * int
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>