package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.12.0.0.12.1.tbz
sha256=08a12e8e8766c2e6a6a7394b0df48989c081367fa7d4d8dd8cdcd026575b4859
sha512=80267021f065f04543f72f16827fc7642ce98ed93940b0f780e83b0c751ac1a8df0e27018326315726c1b7b029015da31eec8322fda15a3a23c57850d53ef358
doc/serlib_setoid_ring/Serlib_setoid_ring/Ser_g_newring/index.html
Module Serlib_setoid_ring.Ser_g_newring
module CAst = Serlib.Ser_cAst
module Libnames = Serlib.Ser_libnames
module Constrexpr = Serlib.Ser_constrexpr
module Tactypes = Serlib.Ser_tactypes
module Genintern = Serlib.Ser_genintern
module EConstr = Serlib.Ser_eConstr
module Tacexpr = Serlib_ltac.Ser_tacexpr
module Ltac_plugin : sig ... end
val coeff_spec_of_sexp :
'constr. (Ppx_sexp_conv_lib.Sexp.t -> 'constr) ->
Ppx_sexp_conv_lib.Sexp.t ->
'constr coeff_spec
val sexp_of_coeff_spec :
'constr. ('constr -> Ppx_sexp_conv_lib.Sexp.t) ->
'constr coeff_spec ->
Ppx_sexp_conv_lib.Sexp.t
type cst_tac_spec = Newring_plugin.Newring_ast.cst_tac_spec =
| CstTac of Ltac_plugin.Tacexpr.raw_tactic_expr
| Closed of Libnames.qualid list
val cst_tac_spec_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> cst_tac_spec
val sexp_of_cst_tac_spec : cst_tac_spec -> Ppx_sexp_conv_lib.Sexp.t
type 'constr ring_mod = 'constr Newring_plugin.Newring_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
val ring_mod_of_sexp :
'constr. (Ppx_sexp_conv_lib.Sexp.t -> 'constr) ->
Ppx_sexp_conv_lib.Sexp.t ->
'constr ring_mod
val sexp_of_ring_mod :
'constr. ('constr -> Ppx_sexp_conv_lib.Sexp.t) ->
'constr ring_mod ->
Ppx_sexp_conv_lib.Sexp.t
type 'a field_mod = 'a Newring_plugin.Newring_ast.field_mod =
| Ring_mod of 'a ring_mod
| Inject of Constrexpr.constr_expr
val field_mod_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a field_mod
val sexp_of_field_mod :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a field_mod ->
Ppx_sexp_conv_lib.Sexp.t
val ser_wit_field_mod :
(Constrexpr.constr_expr field_mod, unit, unit) Serlib.Ser_genarg.gen_ser
val ser_wit_field_mods :
(Constrexpr.constr_expr field_mod list, unit, unit) Serlib.Ser_genarg.gen_ser
val ser_wit_ring_mod :
(Constrexpr.constr_expr ring_mod, unit, unit) Serlib.Ser_genarg.gen_ser
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)"
>