Skip to content

Guarantees

module Guarantees
Assembly Nacara.Plugin.Rocq

The index page: the project's titled theorems, sorted by what their proofs establish.

Declared inside
Entry A theorem on the index page
Group The status of a theorem, as its source and navigator.json state it

Functions and values

entries (project: RocqProject) (links: Links) (config: Config) (facts: Facts option) : Entry array

An entry for each Theorem and Corollary whose attached (**md comment opens with a line wholly in bold, in project order.

Without a suffix or marker in config, the Falsified or Check group stays empty. The first matching group in the order of Group wins.

toHtml (entries: Entry array) : string

The index page's HTML: each non-empty group under its heading, with entries under their module.