Module `Serlib.Ser_tactypes`Source

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 =

| 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

Sourceand '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

Sourceand '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. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a intro_pattern_action_expr

Source

val intro_pattern_expr_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a intro_pattern_expr

Source

val or_and_intro_pattern_expr_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a or_and_intro_pattern_expr

Source

val sexp_of_intro_pattern_action_expr : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a intro_pattern_action_expr ->
  Sexplib0.Sexp.t

Source

val sexp_of_intro_pattern_expr : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a intro_pattern_expr ->
  Sexplib0.Sexp.t

Source

val sexp_of_or_and_intro_pattern_expr : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a or_and_intro_pattern_expr ->
  Sexplib0.Sexp.t

Source

val intro_pattern_action_expr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a intro_pattern_action_expr ->
  Yojson.Safe.t

Source

val intro_pattern_action_expr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a intro_pattern_action_expr Ppx_deriving_yojson_runtime.error_or

Source

val intro_pattern_expr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a intro_pattern_expr ->
  Yojson.Safe.t

Source

val intro_pattern_expr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a intro_pattern_expr Ppx_deriving_yojson_runtime.error_or

Source

val or_and_intro_pattern_expr_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a or_and_intro_pattern_expr ->
  Yojson.Safe.t

Source

val or_and_intro_pattern_expr_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a or_and_intro_pattern_expr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_intro_pattern_action_expr : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a intro_pattern_action_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_fold_intro_pattern_expr : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a intro_pattern_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_fold_or_and_intro_pattern_expr : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a or_and_intro_pattern_expr ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_intro_pattern_action_expr : 
  'a. ('a -> 'a -> int) ->
  'a intro_pattern_action_expr ->
  'a intro_pattern_action_expr ->
  int

Source

val compare_intro_pattern_expr : 
  'a. ('a -> 'a -> int) ->
  'a intro_pattern_expr ->
  'a intro_pattern_expr ->
  int

Source

val compare_or_and_intro_pattern_expr : 
  'a. ('a -> 'a -> int) ->
  'a or_and_intro_pattern_expr ->
  'a or_and_intro_pattern_expr ->
  int

Sourcetype quantified_hypothesis = Tactypes.quantified_hypothesis =

| AnonHyp of int
| NamedHyp of Names.lident

Sourceval quantified_hypothesis_of_sexp : Sexplib0.Sexp.t -> quantified_hypothesis

Sourceval sexp_of_quantified_hypothesis : quantified_hypothesis -> Sexplib0.Sexp.t

Sourceval quantified_hypothesis_to_yojson : quantified_hypothesis -> Yojson.Safe.t

Source

val quantified_hypothesis_of_yojson : 
  Yojson.Safe.t ->
  quantified_hypothesis Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_quantified_hypothesis : 
  Ppx_hash_lib.Std.Hash.state ->
  quantified_hypothesis ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_quantified_hypothesis : 
  quantified_hypothesis ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_quantified_hypothesis : 
  quantified_hypothesis ->
  quantified_hypothesis ->
  int

Sourcetype 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list

Source

val explicit_bindings_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a explicit_bindings

Source

val sexp_of_explicit_bindings : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a explicit_bindings ->
  Sexplib0.Sexp.t

Source

val explicit_bindings_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a explicit_bindings ->
  Yojson.Safe.t

Source

val explicit_bindings_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a explicit_bindings Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_explicit_bindings : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a explicit_bindings ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_explicit_bindings : 
  'a. ('a -> 'a -> int) ->
  'a explicit_bindings ->
  'a explicit_bindings ->
  int

Sourcetype 'a bindings = 'a Tactypes.bindings =

| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings

Source

val bindings_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a bindings

Source

val sexp_of_bindings : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a bindings ->
  Sexplib0.Sexp.t

Source

val bindings_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a bindings ->
  Yojson.Safe.t

Source

val bindings_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a bindings Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_bindings : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a bindings ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_bindings : 
  'a. ('a -> 'a -> int) ->
  'a bindings ->
  'a bindings ->
  int

Sourcetype 'a with_bindings = 'a * 'a bindings

Source

val with_bindings_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a with_bindings

Source

val sexp_of_with_bindings : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a with_bindings ->
  Sexplib0.Sexp.t

Source

val with_bindings_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a with_bindings ->
  Yojson.Safe.t

Source

val with_bindings_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a with_bindings Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_with_bindings : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a with_bindings ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_with_bindings : 
  'a. ('a -> 'a -> int) ->
  'a with_bindings ->
  'a with_bindings ->
  int

Sourcemodule DO : sig ... end

Sourcemodule B : sig ... end

Sourcetype 'a delayed_open = 'a B.t

Source

val delayed_open_of_sexp : 
  'a. (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a delayed_open

Source

val sexp_of_delayed_open : 
  'a. ('a -> Sexplib0.Sexp.t) ->
  'a delayed_open ->
  Sexplib0.Sexp.t

Source

val delayed_open_to_yojson : 
  'a. ('a -> Yojson.Safe.t) ->
  'a delayed_open ->
  Yojson.Safe.t

Source

val delayed_open_of_yojson : 
  'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a delayed_open Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_delayed_open : 
  'a. (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
  Ppx_hash_lib.Std.Hash.state ->
  'a delayed_open ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_delayed_open : 
  'a. ('a -> 'a -> int) ->
  'a delayed_open ->
  'a delayed_open ->
  int

Sourcetype delayed_open_constr = EConstr.constr delayed_open

Sourceval delayed_open_constr_of_sexp : Sexplib0.Sexp.t -> delayed_open_constr

Sourceval sexp_of_delayed_open_constr : delayed_open_constr -> Sexplib0.Sexp.t

Sourceval delayed_open_constr_to_yojson : delayed_open_constr -> Yojson.Safe.t

Source

val delayed_open_constr_of_yojson : 
  Yojson.Safe.t ->
  delayed_open_constr Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_delayed_open_constr : 
  Ppx_hash_lib.Std.Hash.state ->
  delayed_open_constr ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_delayed_open_constr : 
  delayed_open_constr ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_delayed_open_constr : 
  delayed_open_constr ->
  delayed_open_constr ->
  int

Source

type delayed_open_constr_with_bindings =
  EConstr.constr with_bindings delayed_open

Source

val delayed_open_constr_with_bindings_of_sexp : 
  Sexplib0.Sexp.t ->
  delayed_open_constr_with_bindings

Source

val sexp_of_delayed_open_constr_with_bindings : 
  delayed_open_constr_with_bindings ->
  Sexplib0.Sexp.t

Source

val delayed_open_constr_with_bindings_to_yojson : 
  delayed_open_constr_with_bindings ->
  Yojson.Safe.t

Source

val delayed_open_constr_with_bindings_of_yojson : 
  Yojson.Safe.t ->
  delayed_open_constr_with_bindings Ppx_deriving_yojson_runtime.error_or

Source

val _ : 
  Yojson.Safe.t ->
  delayed_open_constr_with_bindings Ppx_deriving_yojson_runtime.error_or

Source

val hash_fold_delayed_open_constr_with_bindings : 
  Ppx_hash_lib.Std.Hash.state ->
  delayed_open_constr_with_bindings ->
  Ppx_hash_lib.Std.Hash.state

Source

val hash_delayed_open_constr_with_bindings : 
  delayed_open_constr_with_bindings ->
  Ppx_hash_lib.Std.Hash.hash_value

Source

val compare_delayed_open_constr_with_bindings : 
  delayed_open_constr_with_bindings ->
  delayed_open_constr_with_bindings ->
  int

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Serlib.Ser_tactypes`Source

package coq-lsp

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Serlib.Ser_tactypesSource

Module `Serlib.Ser_tactypes`Source