package coq-lsp

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

Module Coq.StateSource

Sourcetype t
Sourceval compare : t -> t -> int
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval mode : st:t -> Pvernac.proof_mode option
Sourceval parsing : st:t -> Procq.frozen_t
Sourcemodule Proof : sig ... end

Proof states

Sourceval lemmas : st:t -> Proof.t option
Sourceval program : st:t -> Declare.OblState.View.t Names.Id.Map.t
Sourceval in_state : token:Limits.Token.t -> st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.t

Execute a command in state st. Unfortunately this can produce anomalies as Coq state setting is imperative, so we need to wrap it in protect.

Sourceval in_stateM : token:Limits.Token.t -> st:t -> f:('a -> ('b, Loc.t) Protect.E.t) -> 'a -> ('b, Loc.t) Protect.E.t

Execute a monadic command in state st.

Sourceval drop_proof : st:t -> t

Drop the top proof from the state

Sourceval drop_all_proofs : st:t -> t

Drop all proofs from the state

Sourceval admit : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t

Fully admit an ongoing proof

Sourceval admit_goal : token:Limits.Token.t -> st:t -> (t, Loc.t) Protect.E.t

Admit the current sub-goal

Sourceval info_universes : token:Limits.Token.t -> st:t -> (int * int, Loc.t) Protect.E.t

Info about universes

Sourceval marshal_in : in_channel -> t

Extra / interanl

Sourceval marshal_out : out_channel -> t -> unit
Sourceval of_coq : Vernacstate.t -> t
Sourceval to_coq : t -> Vernacstate.t
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