package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.10.0.0.7.2.tbz
sha256=39018932b0520cc042246a3f9e03f3788d1aaff65568b480d8681cba235032e9
sha512=62a3bb3950e5f9d9cfa5fca85a1108a04fd8c1833cba560ff9d52246ef96d3d61a4743e6dc6d52f53c6a495040fad53f1d9aae383609227a6eb84568ad2a1a6c
doc/coq-serapi.serlib/Serlib/Ser_tactypes/index.html
Module Serlib.Ser_tactypes
module CAst = Ser_cAstmodule Names = Ser_namesmodule Namegen = Ser_namegenmodule EConstr = Ser_eConstrtype 'a intro_pattern_action_expr = 'a Tactypes.intro_pattern_action_expr = | IntroWildcard| IntroOrAndPattern of 'a or_and_intro_pattern_expr| IntroInjection of 'a intro_pattern_expr CAst.t list| IntroApplyOn of 'a CAst.t * 'a intro_pattern_expr CAst.t| IntroRewrite of bool
and 'a intro_pattern_expr = 'a Tactypes.intro_pattern_expr = | IntroForthcoming of bool| IntroNaming of Namegen.intro_pattern_naming_expr| IntroAction of 'a intro_pattern_action_expr
and 'a or_and_intro_pattern_expr = 'a Tactypes.or_and_intro_pattern_expr = | IntroOrPattern of 'a intro_pattern_expr CAst.t list list| IntroAndPattern of 'a intro_pattern_expr CAst.t list
val intro_pattern_action_expr_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a intro_pattern_action_exprval intro_pattern_expr_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a intro_pattern_exprval or_and_intro_pattern_expr_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a or_and_intro_pattern_exprval sexp_of_intro_pattern_action_expr :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a intro_pattern_action_expr ->
Ppx_sexp_conv_lib.Sexp.tval sexp_of_intro_pattern_expr :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a intro_pattern_expr ->
Ppx_sexp_conv_lib.Sexp.tval sexp_of_or_and_intro_pattern_expr :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a or_and_intro_pattern_expr ->
Ppx_sexp_conv_lib.Sexp.ttype quantified_hypothesis = Tactypes.quantified_hypothesis = | AnonHyp of int| NamedHyp of Names.Id.t
val quantified_hypothesis_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
quantified_hypothesisval sexp_of_quantified_hypothesis :
quantified_hypothesis ->
Ppx_sexp_conv_lib.Sexp.ttype 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t listval explicit_bindings_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a explicit_bindingsval sexp_of_explicit_bindings :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a explicit_bindings ->
Ppx_sexp_conv_lib.Sexp.ttype 'a bindings = 'a Tactypes.bindings = | ImplicitBindings of 'a list| ExplicitBindings of 'a explicit_bindings| NoBindings
val bindings_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a bindingsval sexp_of_bindings :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a bindings ->
Ppx_sexp_conv_lib.Sexp.ttype 'a with_bindings = 'a * 'a bindingsval with_bindings_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a with_bindingsval sexp_of_with_bindings :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a with_bindings ->
Ppx_sexp_conv_lib.Sexp.tval sexp_of_delayed_open : 'a -> 'b -> Sexplib.Sexp.tval delayed_open_of_sexp : 'a -> Sexplib.Sexp.t -> 'btype delayed_open_constr = EConstr.constr delayed_openval delayed_open_constr_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
delayed_open_constrval sexp_of_delayed_open_constr :
delayed_open_constr ->
Ppx_sexp_conv_lib.Sexp.ttype delayed_open_constr_with_bindings =
EConstr.constr with_bindings delayed_openval delayed_open_constr_with_bindings_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
delayed_open_constr_with_bindingsval sexp_of_delayed_open_constr_with_bindings :
delayed_open_constr_with_bindings ->
Ppx_sexp_conv_lib.Sexp.t