package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
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) ref

trace header extra message

val message_ref : (lvl:Fleche.Io.Level.t -> message:string -> unit) 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.

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