package coq-lsp

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Require evaluation cache, also invariant w.r.t. locations inside Coq.Ast.Require.t

type output = Coq.State.t

For now, to generalize later if needed

eval i Eval an input i

eval i Eval an input i and produce stats

val size : unit -> int

size () Return the cache size in words, expensive

val all_freqs : unit -> int list

freqs (): (sorted) histogram

val stats : unit -> Hashtbl.statistics

stats (): hashtbl stats

val input_info : input -> string

debug data for input

val clear : unit -> unit

clears the cache

OCaml

Innovation. Community. Security.