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_univ/index.html
Module Serlib.Ser_univ
Source
Source
val constraint_type_of_yojson :
Yojson.Safe.t ->
constraint_type Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_constraint_type :
Ppx_hash_lib.Std.Hash.state ->
constraint_type ->
Ppx_hash_lib.Std.Hash.state
A value in a universe context (resp. context set).
Source
val in_universe_context_of_sexp :
(Sexplib.Sexp.t -> 'a) ->
Sexplib.Sexp.t ->
'a in_universe_context
Source
val sexp_of_in_universe_context :
('a -> Sexplib.Sexp.t) ->
'a in_universe_context ->
Sexplib.Sexp.t
Source
val in_universe_context_set_of_sexp :
(Sexplib.Sexp.t -> 'a) ->
Sexplib.Sexp.t ->
'a in_universe_context_set
Source
val sexp_of_in_universe_context_set :
('a -> Sexplib.Sexp.t) ->
'a in_universe_context_set ->
Sexplib.Sexp.t
Source
val puniverses_of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a puniverses Ppx_deriving_yojson_runtime.error_or
Source
val hash_fold_puniverses :
(Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
Ppx_hash_lib.Std.Hash.state ->
'a puniverses ->
Ppx_hash_lib.Std.Hash.state
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>