package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.13.0.0.13.1.tbz
sha256=530991b3e029102367184b96d8bd8a347c7172265a5815176a533b1061f8c6cf
sha512=c6cc5afcad3546c3fbcd8512f20a5ebd748f17529805c1d296959092fde8f31b77f7c7a06254f68c30eb6c6ad520bfbf03388505186a600e75d65ae3acd02c77

doc/coq-serapi.serlib/Serlib/Ser_tactypes/index.html

Module Serlib.Ser_tactypesSource

Sourcemodule CAst = Ser_cAst
Sourcemodule Names = Ser_names
Sourcemodule Namegen = Ser_namegen
Sourcemodule EConstr = Ser_eConstr
Sourcetype 'a intro_pattern_action_expr = 'a Tactypes.intro_pattern_action_expr =
  1. | IntroWildcard
  2. | IntroOrAndPattern of 'a or_and_intro_pattern_expr
  3. | IntroInjection of 'a intro_pattern_expr CAst.t list
  4. | IntroApplyOn of 'a CAst.t * 'a intro_pattern_expr CAst.t
  5. | IntroRewrite of bool
Sourceand 'a intro_pattern_expr = 'a Tactypes.intro_pattern_expr =
  1. | IntroForthcoming of bool
  2. | IntroNaming of Namegen.intro_pattern_naming_expr
  3. | IntroAction of 'a intro_pattern_action_expr
Sourceand 'a or_and_intro_pattern_expr = 'a Tactypes.or_and_intro_pattern_expr =
  1. | IntroOrPattern of 'a intro_pattern_expr CAst.t list list
  2. | IntroAndPattern of 'a intro_pattern_expr CAst.t list
Sourceval intro_pattern_action_expr_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a intro_pattern_action_expr
Sourceval intro_pattern_expr_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a intro_pattern_expr
Sourceval 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_expr
Sourceval sexp_of_intro_pattern_action_expr : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a intro_pattern_action_expr -> Ppx_sexp_conv_lib.Sexp.t
Sourceval sexp_of_intro_pattern_expr : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a intro_pattern_expr -> Ppx_sexp_conv_lib.Sexp.t
Sourceval 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.t
Sourcetype quantified_hypothesis = Tactypes.quantified_hypothesis =
  1. | AnonHyp of int
  2. | NamedHyp of Names.Id.t
Sourceval quantified_hypothesis_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> quantified_hypothesis
Sourceval sexp_of_quantified_hypothesis : quantified_hypothesis -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
Sourceval explicit_bindings_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a explicit_bindings
Sourceval sexp_of_explicit_bindings : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a explicit_bindings -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype 'a bindings = 'a Tactypes.bindings =
  1. | ImplicitBindings of 'a list
  2. | ExplicitBindings of 'a explicit_bindings
  3. | NoBindings
Sourceval bindings_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a bindings
Sourceval sexp_of_bindings : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a bindings -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype 'a with_bindings = 'a * 'a bindings
Sourceval with_bindings_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a with_bindings
Sourceval sexp_of_with_bindings : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a with_bindings -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
Sourceval sexp_of_delayed_open : 'a -> 'b -> Sexplib.Sexp.t
Sourceval delayed_open_of_sexp : 'a -> Sexplib.Sexp.t -> 'b
Sourcetype delayed_open_constr = EConstr.constr delayed_open
Sourceval delayed_open_constr_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> delayed_open_constr
Sourceval sexp_of_delayed_open_constr : delayed_open_constr -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
Sourceval delayed_open_constr_with_bindings_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> delayed_open_constr_with_bindings
Sourceval sexp_of_delayed_open_constr_with_bindings : delayed_open_constr_with_bindings -> Ppx_sexp_conv_lib.Sexp.t