coq-serapi 8.19.0+0.19.0 · OCaml Package

type subscopes = Notation_term.subscopes

val sexp_of_subscopes : subscopes -> Sexplib0.Sexp.t

val subscopes_of_sexp : Sexplib0.Sexp.t -> subscopes

val subscopes_to_yojson : subscopes -> Yojson.Safe.t

val subscopes_of_yojson : 
  Yojson.Safe.t ->
  subscopes Ppx_deriving_yojson_runtime.error_or

val hash_fold_subscopes : Base.Hash.state -> subscopes -> Base.Hash.state

val hash_subscopes : subscopes -> Base.Hash.hash_value

val compare_subscopes : subscopes -> subscopes -> int

type notation_binder_kind = Notation_term.notation_binder_kind

val sexp_of_notation_binder_kind : notation_binder_kind -> Sexplib0.Sexp.t

val notation_binder_kind_of_sexp : Sexplib0.Sexp.t -> notation_binder_kind

val notation_binder_kind_to_yojson : notation_binder_kind -> Yojson.Safe.t

val notation_binder_kind_of_yojson : 
  Yojson.Safe.t ->
  notation_binder_kind Ppx_deriving_yojson_runtime.error_or

val hash_fold_notation_binder_kind : 
  Base.Hash.state ->
  notation_binder_kind ->
  Base.Hash.state

val hash_notation_binder_kind : notation_binder_kind -> Base.Hash.hash_value

val compare_notation_binder_kind : 
  notation_binder_kind ->
  notation_binder_kind ->
  int

type notation_var_internalization_type =
  Notation_term.notation_var_internalization_type

val sexp_of_notation_var_internalization_type : 
  notation_var_internalization_type ->
  Sexplib0.Sexp.t

val notation_var_internalization_type_of_sexp : 
  Sexplib0.Sexp.t ->
  notation_var_internalization_type

val notation_var_internalization_type_to_yojson : 
  notation_var_internalization_type ->
  Yojson.Safe.t

val notation_var_internalization_type_of_yojson : 
  Yojson.Safe.t ->
  notation_var_internalization_type Ppx_deriving_yojson_runtime.error_or

val hash_fold_notation_var_internalization_type : 
  Base.Hash.state ->
  notation_var_internalization_type ->
  Base.Hash.state

val hash_notation_var_internalization_type : 
  notation_var_internalization_type ->
  Base.Hash.hash_value

val compare_notation_var_internalization_type : 
  notation_var_internalization_type ->
  notation_var_internalization_type ->
  int

type notation_var_binders = Notation_term.notation_var_binders

val sexp_of_notation_var_binders : notation_var_binders -> Sexplib0.Sexp.t

val notation_var_binders_of_sexp : Sexplib0.Sexp.t -> notation_var_binders

val notation_var_binders_to_yojson : notation_var_binders -> Yojson.Safe.t

val notation_var_binders_of_yojson : 
  Yojson.Safe.t ->
  notation_var_binders Ppx_deriving_yojson_runtime.error_or

val hash_fold_notation_var_binders : 
  Base.Hash.state ->
  notation_var_binders ->
  Base.Hash.state

val hash_notation_var_binders : notation_var_binders -> Base.Hash.hash_value

val compare_notation_var_binders : 
  notation_var_binders ->
  notation_var_binders ->
  int

package coq-serapi