package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (35)

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.1.7.8.17.tbz
sha256=efb85d6656abfd26d2c6fd5e69c9b6428b72679d13ee34c493b4253e345b1c8f
sha512=71a47460bab8781bc9f24bae0369b463a9d527a96f1a32eb5752172316f1bdc1941e0430e79d775b61d854a7306ba8f97707c4e406d02bdf8b2ad57877c5e690

doc/coq-lsp.coq/Coq/Goals/index.html

Module Coq.GoalsSource

Sourcetype 'a hyp = {
  1. names : string list;
    (*

    This will become Names.Id.t list in 0.2.0

    *)
  2. def : 'a option;
  3. ty : 'a;
}
Sourcetype info = {
  1. evar : Evar.t;
  2. name : Names.Id.t option;
}
Sourcetype 'a reified_goal = {
  1. info : info;
  2. hyps : 'a hyp list;
  3. ty : 'a;
}
Sourceval map_reified_goal : f:('a -> 'b) -> 'a reified_goal -> 'b reified_goal
Sourcetype ('a, 'pp) goals = {
  1. goals : 'a list;
  2. stack : ('a list * 'a list) list;
  3. bullet : 'pp option;
  4. shelf : 'a list;
  5. given_up : 'a list;
}
Sourceval map_goals : f:('a -> 'b) -> ('a, 'pp) goals -> ('b, 'pp) goals
Sourcetype 'pp reified_pp = ('pp reified_goal, 'pp) goals
Sourceval reify : ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'pp) -> State.Proof.t -> ('pp reified_goal, Pp.t) goals

Stm-independent goal processor