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.0.tbz
sha256=5cd48e23a8893f71f7b599dc919ce52d19eb4a6feeaa49f954e0a7123496a306
sha512=cc09f481c5dfdf181711aa13ef1d93176b4143a14ef863375f98e25db15da8ed4335526a27ba33479594a0bd745733eaaf02437ce7e0f972d97673b04d25773c
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)"
>