package coq-serapi

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

Install

Dune 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.15.0.0.15.1.tbz
sha256=31d1e4661f5b1b917d7004c749cc05eb73546d3190ac632faddc37348531a0a5
sha512=a9816915f9dc4051e76c5b0e615b27c1bb0a6a5ffd445af94ad2ed1582a0e704a7f49f69b6764fa92dbfa092aa8e41ee3151a1330b394eb0338c796d6460fa20

doc/serlib_ltac/Serlib_ltac/Ser_tacexpr/index.html

Module Serlib_ltac.Ser_tacexprSource

Sourcetype direction_flag = bool
Sourceval direction_flag_of_sexp : Sexplib.Sexp.t -> direction_flag
Sourceval sexp_of_direction_flag : direction_flag -> Sexplib.Sexp.t
Sourcetype lazy_flag = Ltac_plugin.Tacexpr.lazy_flag =
  1. | General
  2. | Select
  3. | Once
Sourceval lazy_flag_of_sexp : Sexplib.Sexp.t -> lazy_flag
Sourceval sexp_of_lazy_flag : lazy_flag -> Sexplib.Sexp.t
Sourcetype global_flag = Ltac_plugin.Tacexpr.global_flag =
  1. | TacGlobal
  2. | TacLocal
Sourceval global_flag_of_sexp : Sexplib.Sexp.t -> global_flag
Sourceval sexp_of_global_flag : global_flag -> Sexplib.Sexp.t
Sourcetype evars_flag = bool
Sourceval evars_flag_of_sexp : Sexplib.Sexp.t -> evars_flag
Sourceval sexp_of_evars_flag : evars_flag -> Sexplib.Sexp.t
Sourcetype rec_flag = bool
Sourceval rec_flag_of_sexp : Sexplib.Sexp.t -> rec_flag
Sourceval sexp_of_rec_flag : rec_flag -> Sexplib.Sexp.t
Sourcetype advanced_flag = bool
Sourceval advanced_flag_of_sexp : Sexplib.Sexp.t -> advanced_flag
Sourceval sexp_of_advanced_flag : advanced_flag -> Sexplib.Sexp.t
Sourcetype letin_flag = bool
Sourceval letin_flag_of_sexp : Sexplib.Sexp.t -> letin_flag
Sourceval sexp_of_letin_flag : letin_flag -> Sexplib.Sexp.t
Sourcetype clear_flag = bool option
Sourceval clear_flag_of_sexp : Sexplib.Sexp.t -> clear_flag
Sourceval sexp_of_clear_flag : clear_flag -> Sexplib.Sexp.t
Sourcetype ('c, 'd, 'id) inversion_strength = ('c, 'd, 'id) Ltac_plugin.Tacexpr.inversion_strength
Sourceval inversion_strength_of_sexp : (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('c, 'd, 'id) inversion_strength
Sourceval sexp_of_inversion_strength : ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('c, 'd, 'id) inversion_strength -> Sexplib.Sexp.t
Sourcetype ('a, 'b) location = ('a, 'b) Ltac_plugin.Tacexpr.location =
  1. | HypLocation of 'a
  2. | ConclLocation of 'b
Sourceval location_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'b) -> Sexplib.Sexp.t -> ('a, 'b) location
Sourceval sexp_of_location : ('a -> Sexplib.Sexp.t) -> ('b -> Sexplib.Sexp.t) -> ('a, 'b) location -> Sexplib.Sexp.t
Sourcetype 'id message_token = 'id Ltac_plugin.Tacexpr.message_token
Sourceval message_token_of_sexp : (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> 'id message_token
Sourceval sexp_of_message_token : ('id -> Sexplib.Sexp.t) -> 'id message_token -> Sexplib.Sexp.t
Sourcetype ('dconstr, 'id) induction_clause = ('dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause
Sourceval induction_clause_of_sexp : (Sexplib.Sexp.t -> 'dconstr) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('dconstr, 'id) induction_clause
Sourceval sexp_of_induction_clause : ('dconstr -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('dconstr, 'id) induction_clause -> Sexplib.Sexp.t
Sourcetype ('constr, 'dconstr, 'id) induction_clause_list = ('constr, 'dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause_list
Sourceval induction_clause_list_of_sexp : (Sexplib.Sexp.t -> 'constr) -> (Sexplib.Sexp.t -> 'dconstr) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('constr, 'dconstr, 'id) induction_clause_list
Sourceval sexp_of_induction_clause_list : ('constr -> Sexplib.Sexp.t) -> ('dconstr -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('constr, 'dconstr, 'id) induction_clause_list -> Sexplib.Sexp.t
Sourcetype 'a with_bindings_arg = 'a Ltac_plugin.Tacexpr.with_bindings_arg
Sourceval with_bindings_arg_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_bindings_arg
Sourceval sexp_of_with_bindings_arg : ('a -> Sexplib.Sexp.t) -> 'a with_bindings_arg -> Sexplib.Sexp.t
Sourcetype 'a match_pattern = 'a Ltac_plugin.Tacexpr.match_pattern
Sourceval match_pattern_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_pattern
Sourceval sexp_of_match_pattern : ('a -> Sexplib.Sexp.t) -> 'a match_pattern -> Sexplib.Sexp.t
Sourcetype 'a match_context_hyps = 'a Ltac_plugin.Tacexpr.match_context_hyps
Sourceval match_context_hyps_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_context_hyps
Sourceval sexp_of_match_context_hyps : ('a -> Sexplib.Sexp.t) -> 'a match_context_hyps -> Sexplib.Sexp.t
Sourcetype ('a, 't) match_rule = ('a, 't) Ltac_plugin.Tacexpr.match_rule
Sourceval match_rule_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 't) -> Sexplib.Sexp.t -> ('a, 't) match_rule
Sourceval sexp_of_match_rule : ('a -> Sexplib.Sexp.t) -> ('t -> Sexplib.Sexp.t) -> ('a, 't) match_rule -> Sexplib.Sexp.t
Sourcetype ml_tactic_name = Ltac_plugin.Tacexpr.ml_tactic_name
Sourceval ml_tactic_name_of_sexp : Sexplib.Sexp.t -> ml_tactic_name
Sourceval sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib.Sexp.t
Sourcetype 'd gen_atomic_tactic_expr = 'd Ltac_plugin.Tacexpr.gen_atomic_tactic_expr
Sourceval sexp_of_gen_atomic_tactic_expr : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_atomic_tactic_expr -> Sexplib.Sexp.t
Sourceval sexp_of_gen_tactic_expr : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_expr -> Sexplib.Sexp.t
Sourceval sexp_of_gen_tactic_arg : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_arg -> Sexplib.Sexp.t
Sourceval sexp_of_gen_fun_ast : ('a -> Sexplib.Sexp.t) -> ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('e -> Sexplib.Sexp.t) -> ('f -> Sexplib.Sexp.t) -> ('g -> Sexplib.Sexp.t) -> ('h -> Sexplib.Sexp.t) -> ('i -> Sexplib.Sexp.t) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_fun_ast -> Sexplib.Sexp.t
Sourceval gen_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_atomic_tactic_expr
Sourceval gen_tactic_expr_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_expr
Sourceval gen_tactic_arg_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_arg
Sourceval gen_fun_ast_of_sexp : Sexplib.Sexp.t -> (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'e) -> (Sexplib.Sexp.t -> 'f) -> (Sexplib.Sexp.t -> 'g) -> (Sexplib.Sexp.t -> 'h) -> (Sexplib.Sexp.t -> 'i) -> < constant : 'e ; dterm : 'c ; level : 'i ; name : 'g ; pattern : 'd ; reference : 'f ; tacexpr : 'h ; term : 'a > Ltac_plugin.Tacexpr.gen_tactic_fun_ast
Sourcetype glob_tactic_expr = Ltac_plugin.Tacexpr.glob_tactic_expr
Sourceval glob_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_tactic_expr
Sourceval sexp_of_glob_tactic_expr : glob_tactic_expr -> Sexplib.Sexp.t
Sourcetype glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr
Sourceval glob_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_atomic_tactic_expr
Sourceval sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexplib.Sexp.t
Sourcetype raw_tactic_expr = Ltac_plugin.Tacexpr.raw_tactic_expr
Sourceval raw_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_tactic_expr
Sourceval sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexplib.Sexp.t
Sourcetype raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr
Sourceval raw_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_atomic_tactic_expr
Sourceval sexp_of_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Sexplib.Sexp.t
Sourcetype atomic_tactic_expr = Ltac_plugin.Tacexpr.atomic_tactic_expr
Sourceval atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> atomic_tactic_expr
Sourceval sexp_of_atomic_tactic_expr : atomic_tactic_expr -> Sexplib.Sexp.t
Sourcetype tacdef_body = Ltac_plugin.Tacexpr.tacdef_body
Sourceval tacdef_body_of_sexp : Sexplib.Sexp.t -> tacdef_body
Sourceval sexp_of_tacdef_body : tacdef_body -> Sexplib.Sexp.t
Sourcetype intro_pattern = Ltac_plugin.Tacexpr.intro_pattern
Sourceval intro_pattern_of_sexp : Sexplib.Sexp.t -> intro_pattern
Sourceval sexp_of_intro_pattern : intro_pattern -> Sexplib.Sexp.t
Sourcetype raw_red_expr = Ltac_plugin.Tacexpr.raw_red_expr
Sourceval raw_red_expr_of_sexp : Sexplib.Sexp.t -> raw_red_expr
Sourceval sexp_of_raw_red_expr : raw_red_expr -> Sexplib.Sexp.t
Sourcetype glob_red_expr = Ltac_plugin.Tacexpr.glob_red_expr
Sourceval glob_red_expr_of_sexp : Sexplib.Sexp.t -> glob_red_expr
Sourceval sexp_of_glob_red_expr : glob_red_expr -> Sexplib.Sexp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct