package coq-lsp

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Petanque.Agent

module State : sig ... end
module Env : sig ... end
module Error : sig ... end

Petanque errors

module R : sig ... end

Petanque results

module Run_result : sig ... end

I/O handling, by default, print to stderr

val trace_ref : (string -> ?extra:string -> string -> unit) Stdlib.ref

trace header extra message

val message_ref : (lvl:Fleche.Io.Level.t -> message:string -> unit) Stdlib.ref

message level message

val init : token:Coq.Limits.Token.t -> debug:bool -> root:Lang.LUri.File.t -> Env.t R.t

init ~debug ~root Initializes Coq, with project and workspace settings from root. root needs to be in URI format. This function needs to be called _once_ before all others.

val start : token:Coq.Limits.Token.t -> env:Env.t -> uri:Lang.LUri.File.t -> thm:string -> State.t R.t

start uri thm start a new proof for theorem thm in file uri.

val run_tac : token:Coq.Limits.Token.t -> st:State.t -> tac:string -> State.t Run_result.t R.t

run_tac ~token ~st ~tac tries to run tac over state st

val goals : token:Coq.Limits.Token.t -> st:State.t -> string Coq.Goals.reified_pp option R.t

goals ~token ~st return the list of goals for a given st

module Premise : sig ... end
val premises : token:Coq.Limits.Token.t -> st:State.t -> Premise.t list R.t

Return the list of defined constants and inductives for a given state. For now we just return their fully qualified name, but more options are of course possible.

OCaml

Innovation. Community. Security.