package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a or_var = 'a Locus.or_var
val sexp_of_or_var : ('a -> Sexplib0.Sexp.t) -> 'a or_var -> Sexplib0.Sexp.t
val or_var_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a or_var
val or_var_to_yojson : ('a -> Yojson.Safe.t) -> 'a or_var -> Yojson.Safe.t
val hash_fold_or_var : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a or_var -> Base.Hash.state
val compare_or_var : ('a -> 'a -> int) -> 'a or_var -> 'a or_var -> int
type 'a occurrences_gen = 'a Locus.occurrences_gen
val sexp_of_occurrences_gen : ('a -> Sexplib0.Sexp.t) -> 'a occurrences_gen -> Sexplib0.Sexp.t
val occurrences_gen_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a occurrences_gen
val occurrences_gen_to_yojson : ('a -> Yojson.Safe.t) -> 'a occurrences_gen -> Yojson.Safe.t
val hash_fold_occurrences_gen : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a occurrences_gen -> Base.Hash.state
val compare_occurrences_gen : ('a -> 'a -> int) -> 'a occurrences_gen -> 'a occurrences_gen -> int
type occurrences_expr = Locus.occurrences_expr
val occurrences_expr_of_sexp : Sexplib.Sexp.t -> occurrences_expr
val sexp_of_occurrences_expr : occurrences_expr -> Sexplib.Sexp.t
type 'a with_occurrences_expr = 'a Locus.with_occurrences_expr
val sexp_of_with_occurrences_expr : ('a -> Sexplib0.Sexp.t) -> 'a with_occurrences_expr -> Sexplib0.Sexp.t
val with_occurrences_expr_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_occurrences_expr
val with_occurrences_expr_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_occurrences_expr -> Yojson.Safe.t
val hash_fold_with_occurrences_expr : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a with_occurrences_expr -> Base.Hash.state
val compare_with_occurrences_expr : ('a -> 'a -> int) -> 'a with_occurrences_expr -> 'a with_occurrences_expr -> int
type 'a with_occurrences = 'a Locus.with_occurrences
val sexp_of_with_occurrences : ('a -> Sexplib0.Sexp.t) -> 'a with_occurrences -> Sexplib0.Sexp.t
val with_occurrences_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a with_occurrences
val with_occurrences_to_yojson : ('a -> Yojson.Safe.t) -> 'a with_occurrences -> Yojson.Safe.t
val hash_fold_with_occurrences : (Base.Hash.state -> 'a -> Base.Hash.state) -> Base.Hash.state -> 'a with_occurrences -> Base.Hash.state
val compare_with_occurrences : ('a -> 'a -> int) -> 'a with_occurrences -> 'a with_occurrences -> int
type occurrences = Locus.occurrences
val sexp_of_occurrences : occurrences -> Sexplib0.Sexp.t
val occurrences_of_sexp : Sexplib0.Sexp.t -> occurrences
val occurrences_to_yojson : occurrences -> Yojson.Safe.t
val hash_fold_occurrences : Base.Hash.state -> occurrences -> Base.Hash.state
val hash_occurrences : occurrences -> Base.Hash.hash_value
val compare_occurrences : occurrences -> occurrences -> int
type hyp_location_flag = Locus.hyp_location_flag
val sexp_of_hyp_location_flag : hyp_location_flag -> Sexplib0.Sexp.t
val hyp_location_flag_of_sexp : Sexplib0.Sexp.t -> hyp_location_flag
val hash_fold_hyp_location_flag : Base.Hash.state -> hyp_location_flag -> Base.Hash.state
val hash_hyp_location_flag : hyp_location_flag -> Base.Hash.hash_value
val compare_hyp_location_flag : hyp_location_flag -> hyp_location_flag -> int
type 'a hyp_location_expr = 'a Locus.hyp_location_expr
val hyp_location_expr_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a hyp_location_expr
val sexp_of_hyp_location_expr : ('a -> Sexplib.Sexp.t) -> 'a hyp_location_expr -> Sexplib.Sexp.t
type 'id clause_expr = 'id Locus.clause_expr
val sexp_of_clause_expr : ('id -> Sexplib0.Sexp.t) -> 'id clause_expr -> Sexplib0.Sexp.t
val clause_expr_of_sexp : (Sexplib0.Sexp.t -> 'id) -> Sexplib0.Sexp.t -> 'id clause_expr
val clause_expr_to_yojson : ('id -> Yojson.Safe.t) -> 'id clause_expr -> Yojson.Safe.t
val hash_fold_clause_expr : (Base.Hash.state -> 'id -> Base.Hash.state) -> Base.Hash.state -> 'id clause_expr -> Base.Hash.state
val compare_clause_expr : ('id -> 'id -> int) -> 'id clause_expr -> 'id clause_expr -> int
type clause = Locus.clause
val clause_of_sexp : Sexplib.Sexp.t -> clause
val sexp_of_clause : clause -> Sexplib.Sexp.t
type clause_atom = Locus.clause_atom
val clause_atom_of_sexp : Sexplib.Sexp.t -> clause_atom
val sexp_of_clause_atom : clause_atom -> Sexplib.Sexp.t
type concrete_clause = Locus.concrete_clause
val concrete_clause_of_sexp : Sexplib.Sexp.t -> concrete_clause
val sexp_of_concrete_clause : concrete_clause -> Sexplib.Sexp.t
type hyp_location = Locus.hyp_location
val sexp_of_hyp_location : hyp_location -> Sexplib0.Sexp.t
val hyp_location_of_sexp : Sexplib0.Sexp.t -> hyp_location
val hyp_location_to_yojson : hyp_location -> Yojson.Safe.t
val hash_fold_hyp_location : Base.Hash.state -> hyp_location -> Base.Hash.state
val hash_hyp_location : hyp_location -> Base.Hash.hash_value
val compare_hyp_location : hyp_location -> hyp_location -> int
type goal_location = Locus.goal_location
val goal_location_of_sexp : Sexplib.Sexp.t -> goal_location
val sexp_of_goal_location : goal_location -> Sexplib.Sexp.t
type simple_clause = Locus.simple_clause
val simple_clause_of_sexp : Sexplib.Sexp.t -> simple_clause
val sexp_of_simple_clause : simple_clause -> Sexplib.Sexp.t
type 'id or_like_first = 'id Locus.or_like_first
val or_like_first_of_sexp : (Sexplib.Sexp.t -> 'id) -> Sexplib.Sexp.t -> 'id or_like_first
val sexp_of_or_like_first : ('id -> Sexplib.Sexp.t) -> 'id or_like_first -> Sexplib.Sexp.t
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