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.1.tbz
sha256=31d1e4661f5b1b917d7004c749cc05eb73546d3190ac632faddc37348531a0a5
sha512=a9816915f9dc4051e76c5b0e615b27c1bb0a6a5ffd445af94ad2ed1582a0e704a7f49f69b6764fa92dbfa092aa8e41ee3151a1330b394eb0338c796d6460fa20
doc/coq-serapi.serlib/Serlib/Ser_tactypes/index.html
Module Serlib.Ser_tactypesSource
Source
type '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
Source
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
Source
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
Source
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_exprSource
val intro_pattern_expr_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a intro_pattern_exprSource
val 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_exprSource
val sexp_of_intro_pattern_action_expr :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a intro_pattern_action_expr ->
Ppx_sexp_conv_lib.Sexp.tSource
val sexp_of_intro_pattern_expr :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a intro_pattern_expr ->
Ppx_sexp_conv_lib.Sexp.tSource
val 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.tSource
type quantified_hypothesis = Tactypes.quantified_hypothesis = | AnonHyp of int| NamedHyp of Names.lident
Source
val explicit_bindings_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a explicit_bindingsSource
val sexp_of_explicit_bindings :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a explicit_bindings ->
Ppx_sexp_conv_lib.Sexp.tSource
type 'a bindings = 'a Tactypes.bindings = | ImplicitBindings of 'a list| ExplicitBindings of 'a explicit_bindings| NoBindings
Source
val with_bindings_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a with_bindingsSource
val sexp_of_with_bindings :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a with_bindings ->
Ppx_sexp_conv_lib.Sexp.tSource
val delayed_open_constr_with_bindings_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
delayed_open_constr_with_bindingsSource
val sexp_of_delayed_open_constr_with_bindings :
delayed_open_constr_with_bindings ->
Ppx_sexp_conv_lib.Sexp.t