package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.13.0.0.13.1.tbz
sha256=530991b3e029102367184b96d8bd8a347c7172265a5815176a533b1061f8c6cf
sha512=c6cc5afcad3546c3fbcd8512f20a5ebd748f17529805c1d296959092fde8f31b77f7c7a06254f68c30eb6c6ad520bfbf03388505186a600e75d65ae3acd02c77
doc/serlib_ring/Serlib_ring/Ser_g_ring/index.html
Module Serlib_ring.Ser_g_ring
Source
Source
val coeff_spec_of_sexp :
'constr. (Ppx_sexp_conv_lib.Sexp.t -> 'constr) ->
Ppx_sexp_conv_lib.Sexp.t ->
'constr coeff_spec
Source
val sexp_of_coeff_spec :
'constr. ('constr -> Ppx_sexp_conv_lib.Sexp.t) ->
'constr coeff_spec ->
Ppx_sexp_conv_lib.Sexp.t
Source
type cst_tac_spec = Ring_plugin.Ring_ast.cst_tac_spec =
| CstTac of Ltac_plugin.Tacexpr.raw_tactic_expr
| Closed of Libnames.qualid list
Source
type 'constr ring_mod = 'constr Ring_plugin.Ring_ast.ring_mod =
| Ring_kind of 'constr coeff_spec
| Const_tac of cst_tac_spec
| Pre_tac of Ltac_plugin.Tacexpr.raw_tactic_expr
| Post_tac of Ltac_plugin.Tacexpr.raw_tactic_expr
| Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr
| Pow_spec of cst_tac_spec * Constrexpr.constr_expr
| Sign_spec of Constrexpr.constr_expr
| Div_spec of Constrexpr.constr_expr
Source
type 'a field_mod = 'a Ring_plugin.Ring_ast.field_mod =
| Ring_mod of 'a ring_mod
| Inject of Constrexpr.constr_expr
Source
val ser_wit_field_mod :
(Constrexpr.constr_expr field_mod, unit, unit) Serlib.Ser_genarg.gen_ser
Source
val ser_wit_field_mods :
(Constrexpr.constr_expr field_mod list, unit, unit) Serlib.Ser_genarg.gen_ser
Source
val ser_wit_ring_mod :
(Constrexpr.constr_expr ring_mod, unit, unit) Serlib.Ser_genarg.gen_ser
Source
val ser_wit_ring_mods :
(Constrexpr.constr_expr ring_mod list, unit, unit) Serlib.Ser_genarg.gen_ser
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>