package vscoq-language-server

  1. Overview
  2. Docs
type proof_statement
val yojson_of_proof_statement : proof_statement -> Ppx_yojson_conv_lib.Yojson.Safe.t
val proof_statement_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> proof_statement
type proof_step
val yojson_of_proof_step : proof_step -> Ppx_yojson_conv_lib.Yojson.Safe.t
val proof_step_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> proof_step
type proof_block
val yojson_of_proof_block : proof_block -> Ppx_yojson_conv_lib.Yojson.Safe.t
val proof_block_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> proof_block
type t
include Ppx_yojson_conv_lib.Yojsonable.S with type t := t
val t_of_yojson : Yojson.Safe.t -> t
val yojson_of_t : t -> Yojson.Safe.t
val get_proof : previous:Vernacstate.t option -> Settings.Goals.Diff.Mode.t -> Vernacstate.t -> t option
val mk_proof_statement : string -> Lsp.Types.Range.t -> proof_statement
val mk_proof_step : string -> Lsp.Types.Range.t -> proof_step
val mk_proof_block : proof_statement -> proof_step list -> Lsp.Types.Range.t -> proof_block
OCaml

Innovation. Community. Security.