Cards
module Cards| Assembly | Nacara.Plugin.Rocq |
The client data files: a card per reference key on a page, and the search index.
Functions and values
badges (project: RocqProject) (facts: Facts option) : int -> Badge option
badges (project: RocqProject) (facts: Facts option) : int -> Badge optionThe badge of a declaration, by its index in RocqProject.Declarations.
Only a theorem with a complete proof and a captured result has one.
forModule (project: RocqProject) (links: Links) (facts: Facts option) (fileIndex: int) : CardData array
forModule (project: RocqProject) (links: Links) (facts: Facts option) (fileIndex: int) : CardData arrayThe contents of a module's symbols.json: a card for each symbol of the file and each reference on its page.
printedBinder (project: RocqProject) (facts: Facts option) : int -> string -> string option
printedBinder (project: RocqProject) (facts: Facts option) : int -> string -> string optionThe type Rocq printed for a binder, by declaration index and binder name.
search (project: RocqProject) (links: Links) (facts: Facts option) : SearchEntry array
search (project: RocqProject) (links: Links) (facts: Facts option) : SearchEntry arrayThe contents of search.json: each declared symbol of the project, in project order.