package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

sha256=31b83f0908bbabf4079806ce9271a30f7af8fb4e2fd5c81c1ccc3c1e8022f0de

sha512=de9f48cb643944620183243a55a225b33b3b77d2cc2ea26e38377622ea9036e7205634e880d804dd0ae69ce22d321ce4dfbacc94aebb402d1f124d5be348ebca

Sourcetype t

Sourceval marshal_in : in_channel -> t

Sourceval marshal_out : out_channel -> t -> unit

Sourceval of_coq : Vernacstate.t -> t

Sourceval to_coq : t -> Vernacstate.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 -> Vernacstate.Parser.t

Sourceval lemmas : st:t -> Vernacstate.LemmaStack.t option

Sourceval in_state : st:t -> f:('a -> 'b) -> 'a -> 'b

Sourceval drop_proofs : st:t -> t

Drop the proofs from the state

Sourceval admit : st:t -> t

Admit an ongoing proof