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.16.0.0.16.2.tbz
sha256=f891507f58fba3ba29889dd07fbe69af3411d246488ae7595cd81d26c8422f14
sha512=224dfda8fae1ead7a5ae2a8ead527834bb5216b1788485a0c19deade3b0dd86767c19056931294a7973f132680e282c4491c76ef38638c0c566a029379f484e2

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 sexp_of_location : ('a -> Sexplib0.Sexp.t) -> ('b -> Sexplib0.Sexp.t) -> ('a, 'b) location -> Sexplib0.Sexp.t
Sourceval location_of_sexp : (Sexplib0.Sexp.t -> 'a) -> (Sexplib0.Sexp.t -> 'b) -> Sexplib0.Sexp.t -> ('a, 'b) location
Sourceval hash_fold_location : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> (Ppx_hash_lib.Std.Hash.state -> 'b -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> ('a, 'b) location -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_location : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) location -> ('a, 'b) location -> int
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 sexp_of_glob_tactic_expr : glob_tactic_expr -> Sexplib0.Sexp.t
Sourceval glob_tactic_expr_of_sexp : Sexplib0.Sexp.t -> glob_tactic_expr
Sourceval glob_tactic_expr_to_yojson : glob_tactic_expr -> Yojson.Safe.t
Sourceval glob_tactic_expr_of_yojson : Yojson.Safe.t -> glob_tactic_expr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_glob_tactic_expr : Ppx_hash_lib.Std.Hash.state -> glob_tactic_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glob_tactic_expr : glob_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glob_tactic_expr : glob_tactic_expr -> glob_tactic_expr -> int
Sourcetype glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr
Sourceval sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexplib0.Sexp.t
Sourceval glob_atomic_tactic_expr_of_sexp : Sexplib0.Sexp.t -> glob_atomic_tactic_expr
Sourceval glob_atomic_tactic_expr_to_yojson : glob_atomic_tactic_expr -> Yojson.Safe.t
Sourceval glob_atomic_tactic_expr_of_yojson : Yojson.Safe.t -> glob_atomic_tactic_expr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_glob_atomic_tactic_expr : Ppx_hash_lib.Std.Hash.state -> glob_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> glob_atomic_tactic_expr -> int
Sourcetype raw_tactic_expr = Ltac_plugin.Tacexpr.raw_tactic_expr
Sourceval sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexplib0.Sexp.t
Sourceval raw_tactic_expr_of_sexp : Sexplib0.Sexp.t -> raw_tactic_expr
Sourceval raw_tactic_expr_to_yojson : raw_tactic_expr -> Yojson.Safe.t
Sourceval raw_tactic_expr_of_yojson : Yojson.Safe.t -> raw_tactic_expr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_tactic_expr : Ppx_hash_lib.Std.Hash.state -> raw_tactic_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_tactic_expr : raw_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_tactic_expr : raw_tactic_expr -> raw_tactic_expr -> int
Sourcetype raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr
Sourceval sexp_of_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Sexplib0.Sexp.t
Sourceval raw_atomic_tactic_expr_of_sexp : Sexplib0.Sexp.t -> raw_atomic_tactic_expr
Sourceval raw_atomic_tactic_expr_to_yojson : raw_atomic_tactic_expr -> Yojson.Safe.t
Sourceval raw_atomic_tactic_expr_of_yojson : Yojson.Safe.t -> raw_atomic_tactic_expr Ppx_deriving_yojson_runtime.error_or
Sourceval hash_fold_raw_atomic_tactic_expr : Ppx_hash_lib.Std.Hash.state -> raw_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> raw_atomic_tactic_expr -> int
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 sexp_of_tacdef_body : tacdef_body -> Sexplib0.Sexp.t
Sourceval tacdef_body_of_sexp : Sexplib0.Sexp.t -> tacdef_body
Sourceval hash_fold_tacdef_body : Ppx_hash_lib.Std.Hash.state -> tacdef_body -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_tacdef_body : tacdef_body -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_tacdef_body : tacdef_body -> tacdef_body -> int
Sourcetype intro_pattern = Ltac_plugin.Tacexpr.intro_pattern
Sourceval sexp_of_intro_pattern : intro_pattern -> Sexplib0.Sexp.t
Sourceval intro_pattern_of_sexp : Sexplib0.Sexp.t -> intro_pattern
Sourceval hash_fold_intro_pattern : Ppx_hash_lib.Std.Hash.state -> intro_pattern -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_intro_pattern : intro_pattern -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_intro_pattern : intro_pattern -> intro_pattern -> int
Sourcetype raw_red_expr = Ltac_plugin.Tacexpr.raw_red_expr
Sourceval sexp_of_raw_red_expr : raw_red_expr -> Sexplib0.Sexp.t
Sourceval raw_red_expr_of_sexp : Sexplib0.Sexp.t -> raw_red_expr
Sourceval hash_fold_raw_red_expr : Ppx_hash_lib.Std.Hash.state -> raw_red_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_red_expr : raw_red_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_red_expr : raw_red_expr -> raw_red_expr -> int
Sourcetype glob_red_expr = Ltac_plugin.Tacexpr.glob_red_expr
Sourceval sexp_of_glob_red_expr : glob_red_expr -> Sexplib0.Sexp.t
Sourceval glob_red_expr_of_sexp : Sexplib0.Sexp.t -> glob_red_expr
Sourceval hash_fold_glob_red_expr : Ppx_hash_lib.Std.Hash.state -> glob_red_expr -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glob_red_expr : glob_red_expr -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glob_red_expr : glob_red_expr -> glob_red_expr -> int
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