Module `Serlib_ltac.Ser_rewrite`Source

Sourcetype unary_strategy = Ltac_plugin.Rewrite.unary_strategy

Sourceval sexp_of_unary_strategy : unary_strategy -> Sexplib0.Sexp.t

Sourceval unary_strategy_of_sexp : Sexplib0.Sexp.t -> unary_strategy

val hash_fold_unary_strategy : 
  Ppx_hash_lib.Std.Hash.state ->
  unary_strategy ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_unary_strategy : unary_strategy -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_unary_strategy : unary_strategy -> unary_strategy -> int

Sourcetype binary_strategy = Ltac_plugin.Rewrite.binary_strategy

Sourceval sexp_of_binary_strategy : binary_strategy -> Sexplib0.Sexp.t

Sourceval binary_strategy_of_sexp : Sexplib0.Sexp.t -> binary_strategy

Source

val hash_fold_binary_strategy : 
  Ppx_hash_lib.Std.Hash.state ->
  binary_strategy ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_binary_strategy : binary_strategy -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_binary_strategy : binary_strategy -> binary_strategy -> int

Sourcetype ('a, 'b) strategy_ast = ('a, 'b) Ltac_plugin.Rewrite.strategy_ast

Source

val sexp_of_strategy_ast : 
  ('a -> Sexplib0.Sexp.t) ->
  ('b -> Sexplib0.Sexp.t) ->
  ('a, 'b) strategy_ast ->
  Sexplib0.Sexp.t

Source

val strategy_ast_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  (Sexplib0.Sexp.t -> 'b) ->
  Sexplib0.Sexp.t ->
  ('a, 'b) strategy_ast

Source

val hash_fold_strategy_ast : 
  (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) strategy_ast ->
  Ppx_hash_lib.Std.Hash.state

Source

val compare_strategy_ast : 
  ('a -> 'a -> int) ->
  ('b -> 'b -> int) ->
  ('a, 'b) strategy_ast ->
  ('a, 'b) strategy_ast ->
  int

Sourcetype strategy = Ltac_plugin.Rewrite.strategy

Sourceval sexp_of_strategy : strategy -> Sexplib0.Sexp.t

Sourceval strategy_of_sexp : Sexplib0.Sexp.t -> strategy

Source

val hash_fold_strategy : 
  Ppx_hash_lib.Std.Hash.state ->
  strategy ->
  Ppx_hash_lib.Std.Hash.state

Sourceval hash_strategy : strategy -> Ppx_hash_lib.Std.Hash.hash_value

Sourceval compare_strategy : strategy -> strategy -> int

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_ltac/Serlib_ltac/Ser_rewrite/index.html

Module `Serlib_ltac.Ser_rewrite`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/serlib_ltac/Serlib_ltac/Ser_rewrite/index.html

Module Serlib_ltac.Ser_rewriteSource

Module `Serlib_ltac.Ser_rewrite`Source