coq-lsp.fleche
Memo.Interp
Example_plugin
coq-lsp.coq
coq-lsp.lang
coq-lsp.lsp
coq-lsp.plugin
fleche_waterproof
type t = Coq.State.t * Coq.Ast.t
val eval : t -> Coq.State.t Coq.Interp.interp_result Stats.t
Interpret a command, possibly memoizing it
val size : unit -> int
size () Return the size in words, expensive
size ()
val input_info : t -> string
debug