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.10.0.0.7.1.tbz
sha256=207b091d8d9d9e1a649759f0acfd15cbfda54a2627a01fc74aa74ec0ffaa3400
sha512=af85d00c5896e78a6edea7794070795ca14c8e47a0e9a28f2ac003364b0f99eb72f19f57e755a3967d255b1aaf62cae0d09bbab02d2d35ef6ee02b84823a0929

doc/serlib_ltac/Ser_tacexpr/index.html

Module Ser_tacexpr

type direction_flag = bool
val direction_flag_of_sexp : Sexplib.Sexp.t -> direction_flag
val sexp_of_direction_flag : direction_flag -> Sexplib.Sexp.t
type lazy_flag = Ltac_plugin.Tacexpr.lazy_flag =
  1. | General
  2. | Select
  3. | Once
val lazy_flag_of_sexp : Sexplib.Sexp.t -> lazy_flag
val sexp_of_lazy_flag : lazy_flag -> Sexplib.Sexp.t
type global_flag = Ltac_plugin.Tacexpr.global_flag =
  1. | TacGlobal
  2. | TacLocal
val global_flag_of_sexp : Sexplib.Sexp.t -> global_flag
val sexp_of_global_flag : global_flag -> Sexplib.Sexp.t
type evars_flag = bool
val evars_flag_of_sexp : Sexplib.Sexp.t -> evars_flag
val sexp_of_evars_flag : evars_flag -> Sexplib.Sexp.t
type rec_flag = bool
val rec_flag_of_sexp : Sexplib.Sexp.t -> rec_flag
val sexp_of_rec_flag : rec_flag -> Sexplib.Sexp.t
type advanced_flag = bool
val advanced_flag_of_sexp : Sexplib.Sexp.t -> advanced_flag
val sexp_of_advanced_flag : advanced_flag -> Sexplib.Sexp.t
type letin_flag = bool
val letin_flag_of_sexp : Sexplib.Sexp.t -> letin_flag
val sexp_of_letin_flag : letin_flag -> Sexplib.Sexp.t
type clear_flag = bool option
val clear_flag_of_sexp : Sexplib.Sexp.t -> clear_flag
val sexp_of_clear_flag : clear_flag -> Sexplib.Sexp.t
type ('c, 'd, 'id) inversion_strength = ('c, 'd, 'id) Ltac_plugin.Tacexpr.inversion_strength
val inversion_strength_of_sexp : (Sexplib.Sexp.t -> 'c) -> (Sexplib.Sexp.t -> 'd) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('c, 'd, 'id) inversion_strength
val sexp_of_inversion_strength : ('c -> Sexplib.Sexp.t) -> ('d -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('c, 'd, 'id) inversion_strength -> Sexplib.Sexp.t
type ('a, 'b) location = ('a, 'b) Ltac_plugin.Tacexpr.location =
  1. | HypLocation of 'a
  2. | ConclLocation of 'b
val location_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 'b) -> Sexplib.Sexp.t -> ('a, 'b) location
val sexp_of_location : ('a -> Sexplib.Sexp.t) -> ('b -> Sexplib.Sexp.t) -> ('a, 'b) location -> Sexplib.Sexp.t
type 'id message_token = 'id Ltac_plugin.Tacexpr.message_token
val message_token_of_sexp : (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> 'id message_token
val sexp_of_message_token : ('id -> Sexplib.Sexp.t) -> 'id message_token -> Sexplib.Sexp.t
type ('dconstr, 'id) induction_clause = ('dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause
val induction_clause_of_sexp : (Sexplib.Sexp.t -> 'dconstr) -> (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> ('dconstr, 'id) induction_clause
val sexp_of_induction_clause : ('dconstr -> Sexplib.Sexp.t) -> ('id -> Sexplib.Sexp.t) -> ('dconstr, 'id) induction_clause -> Sexplib.Sexp.t
type ('constr, 'dconstr, 'id) induction_clause_list = ('constr, 'dconstr, 'id) Ltac_plugin.Tacexpr.induction_clause_list
val 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
val 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
type 'a with_bindings_arg = 'a Ltac_plugin.Tacexpr.with_bindings_arg
val with_bindings_arg_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a with_bindings_arg
val sexp_of_with_bindings_arg : ('a -> Sexplib.Sexp.t) -> 'a with_bindings_arg -> Sexplib.Sexp.t
type 'a match_pattern = 'a Ltac_plugin.Tacexpr.match_pattern
val match_pattern_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_pattern
val sexp_of_match_pattern : ('a -> Sexplib.Sexp.t) -> 'a match_pattern -> Sexplib.Sexp.t
type 'a match_context_hyps = 'a Ltac_plugin.Tacexpr.match_context_hyps
val match_context_hyps_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a match_context_hyps
val sexp_of_match_context_hyps : ('a -> Sexplib.Sexp.t) -> 'a match_context_hyps -> Sexplib.Sexp.t
type ('a, 't) match_rule = ('a, 't) Ltac_plugin.Tacexpr.match_rule
val match_rule_of_sexp : (Sexplib.Sexp.t -> 'a) -> (Sexplib.Sexp.t -> 't) -> Sexplib.Sexp.t -> ('a, 't) match_rule
val sexp_of_match_rule : ('a -> Sexplib.Sexp.t) -> ('t -> Sexplib.Sexp.t) -> ('a, 't) match_rule -> Sexplib.Sexp.t
type ml_tactic_name = Ltac_plugin.Tacexpr.ml_tactic_name
val ml_tactic_name_of_sexp : Sexplib.Sexp.t -> ml_tactic_name
val sexp_of_ml_tactic_name : ml_tactic_name -> Sexplib.Sexp.t
type 'd gen_atomic_tactic_expr = 'd Ltac_plugin.Tacexpr.gen_atomic_tactic_expr
val 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
val 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
val 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
val 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
val 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
val 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
val 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
val 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
type glob_tactic_expr = Ltac_plugin.Tacexpr.glob_tactic_expr
val glob_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_tactic_expr
val sexp_of_glob_tactic_expr : glob_tactic_expr -> Sexplib.Sexp.t
type glob_atomic_tactic_expr = Ltac_plugin.Tacexpr.glob_atomic_tactic_expr
val glob_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> glob_atomic_tactic_expr
val sexp_of_glob_atomic_tactic_expr : glob_atomic_tactic_expr -> Sexplib.Sexp.t
type raw_tactic_expr = Ltac_plugin.Tacexpr.raw_tactic_expr
val raw_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_tactic_expr
val sexp_of_raw_tactic_expr : raw_tactic_expr -> Sexplib.Sexp.t
type raw_atomic_tactic_expr = Ltac_plugin.Tacexpr.raw_atomic_tactic_expr
val raw_atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> raw_atomic_tactic_expr
val sexp_of_raw_atomic_tactic_expr : raw_atomic_tactic_expr -> Sexplib.Sexp.t
type atomic_tactic_expr = Ltac_plugin.Tacexpr.atomic_tactic_expr
val atomic_tactic_expr_of_sexp : Sexplib.Sexp.t -> atomic_tactic_expr
val sexp_of_atomic_tactic_expr : atomic_tactic_expr -> Sexplib.Sexp.t
type tacdef_body = Ltac_plugin.Tacexpr.tacdef_body
val tacdef_body_of_sexp : Sexplib.Sexp.t -> tacdef_body
val sexp_of_tacdef_body : tacdef_body -> Sexplib.Sexp.t
type intro_pattern = Ltac_plugin.Tacexpr.intro_pattern
val intro_pattern_of_sexp : Sexplib.Sexp.t -> intro_pattern
val sexp_of_intro_pattern : intro_pattern -> Sexplib.Sexp.t