coq-serapi 8.12.0+0.12.0 · OCaml Package

type metavariable = Constr.metavariable

val metavariable_of_sexp : Sexplib.Sexp.t -> metavariable

val sexp_of_metavariable : metavariable -> Sexplib.Sexp.t

type pconstant = Constr.pconstant

val pconstant_of_sexp : Sexplib.Sexp.t -> pconstant

val sexp_of_pconstant : pconstant -> Sexplib.Sexp.t

type pinductive = Constr.pinductive

val pinductive_of_sexp : Sexplib.Sexp.t -> pinductive

val sexp_of_pinductive : pinductive -> Sexplib.Sexp.t

type pconstructor = Constr.pconstructor

val pconstructor_of_sexp : Sexplib.Sexp.t -> pconstructor

val sexp_of_pconstructor : pconstructor -> Sexplib.Sexp.t

type cast_kind = Constr.cast_kind

val cast_kind_of_sexp : Sexplib.Sexp.t -> cast_kind

val sexp_of_cast_kind : cast_kind -> Sexplib.Sexp.t

type case_style = Constr.case_style

val case_style_of_sexp : Sexplib.Sexp.t -> case_style

val sexp_of_case_style : case_style -> Sexplib.Sexp.t

val case_style_of_yojson : Yojson.Safe.t -> (case_style, string) Result.result

val case_style_to_yojson : case_style -> Yojson.Safe.t

type case_printing = Constr.case_printing

val case_printing_of_sexp : Sexplib.Sexp.t -> case_printing

val sexp_of_case_printing : case_printing -> Sexplib.Sexp.t

type case_info = Constr.case_info

val case_info_of_sexp : Sexplib.Sexp.t -> case_info

val sexp_of_case_info : case_info -> Sexplib.Sexp.t

type rec_declaration = Constr.rec_declaration

val rec_declaration_of_sexp : Sexplib.Sexp.t -> rec_declaration

val sexp_of_rec_declaration : rec_declaration -> Sexplib.Sexp.t

type fixpoint = Constr.fixpoint

val fixpoint_of_sexp : Sexplib.Sexp.t -> fixpoint

val sexp_of_fixpoint : fixpoint -> Sexplib.Sexp.t

type cofixpoint = Constr.cofixpoint

val cofixpoint_of_sexp : Sexplib.Sexp.t -> cofixpoint

val sexp_of_cofixpoint : cofixpoint -> Sexplib.Sexp.t

type 'constr pexistential = 'constr Constr.pexistential

val pexistential_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  Sexplib.Sexp.t ->
  'constr pexistential

val sexp_of_pexistential : 
  ('constr -> Sexplib.Sexp.t) ->
  'constr pexistential ->
  Sexplib.Sexp.t

type ('constr, 'types) prec_declaration =
  ('constr, 'types) Constr.prec_declaration

val prec_declaration_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  (Sexplib.Sexp.t -> 'types) ->
  Sexplib.Sexp.t ->
  ('constr, 'types) prec_declaration

val sexp_of_prec_declaration : 
  ('constr -> Sexplib.Sexp.t) ->
  ('types -> Sexplib.Sexp.t) ->
  ('constr, 'types) prec_declaration ->
  Sexplib.Sexp.t

type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint

val pfixpoint_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  (Sexplib.Sexp.t -> 'types) ->
  Sexplib.Sexp.t ->
  ('constr, 'types) pfixpoint

val sexp_of_pfixpoint : 
  ('constr -> Sexplib.Sexp.t) ->
  ('types -> Sexplib.Sexp.t) ->
  ('constr, 'types) pfixpoint ->
  Sexplib.Sexp.t

type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint

val pcofixpoint_of_sexp : 
  (Sexplib.Sexp.t -> 'constr) ->
  (Sexplib.Sexp.t -> 'types) ->
  Sexplib.Sexp.t ->
  ('constr, 'types) pcofixpoint

val sexp_of_pcofixpoint : 
  ('constr -> Sexplib.Sexp.t) ->
  ('types -> Sexplib.Sexp.t) ->
  ('constr, 'types) pcofixpoint ->
  Sexplib.Sexp.t

type t = Constr.t

val t_of_sexp : Sexplib.Sexp.t -> t

val sexp_of_t : t -> Sexplib.Sexp.t

val of_yojson : Yojson.Safe.t -> (t, string) Result.result

val to_yojson : t -> Yojson.Safe.t

type constr = t

val constr_of_sexp : Sexplib.Sexp.t -> constr

val sexp_of_constr : constr -> Sexplib.Sexp.t

val constr_of_yojson : Yojson.Safe.t -> (constr, string) Result.result

val constr_to_yojson : constr -> Yojson.Safe.t

type types = constr

val types_of_sexp : Sexplib.Sexp.t -> types

val sexp_of_types : types -> Sexplib.Sexp.t

val types_of_yojson : Yojson.Safe.t -> (types, string) Result.result

val types_to_yojson : types -> Yojson.Safe.t

type existential = Constr.existential

val existential_of_sexp : Sexplib.Sexp.t -> existential

val sexp_of_existential : existential -> Sexplib.Sexp.t

type sorts_family = Sorts.family

val sorts_family_of_sexp : Sexplib.Sexp.t -> sorts_family

val sexp_of_sorts_family : sorts_family -> Sexplib.Sexp.t

type named_declaration = Constr.named_declaration

val named_declaration_of_sexp : Sexplib.Sexp.t -> named_declaration

val sexp_of_named_declaration : named_declaration -> Sexplib.Sexp.t

type named_context = Constr.named_context

val named_context_of_sexp : Sexplib.Sexp.t -> named_context

val sexp_of_named_context : named_context -> Sexplib.Sexp.t

type rel_declaration = Constr.rel_declaration

val rel_declaration_of_sexp : Sexplib.Sexp.t -> rel_declaration

val sexp_of_rel_declaration : rel_declaration -> Sexplib.Sexp.t

type rel_context = Constr.rel_context

val rel_context_of_sexp : Sexplib.Sexp.t -> rel_context

val sexp_of_rel_context : rel_context -> Sexplib.Sexp.t

package coq-serapi