package coq-lsp

  1. Overview
  2. Docs
package coq-lsp
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Petanque.AgentSource

Petanque.Agent

Sourcemodule State : sig ... end
Sourcemodule Env : sig ... end
Sourcemodule Error : sig ... end

Petanque errors

Sourcemodule R : sig ... end

Petanque results

Sourcemodule Run_result : sig ... end

I/O handling, by default, print to stderr

Sourceval trace_ref : (string -> ?extra:string -> string -> unit) ref

trace header extra message

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

message level message

Sourceval 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.

Sourceval 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.

Sourceval 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

Sourceval 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

Sourcemodule Premise : sig ... end
Sourceval 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