Loading source declarations…
definition theorem unprovedColors describe this snapshot’s review status, not correctness certificates. Click a color to filter.How it works
Modules follow coqdep -sort. Within a module, declarations follow the positions recorded in Rocq’s compiled .glob files.
coqdep -sort
.glob
Solid lines show declaration dependencies; dashed lines show source order.
A name match can be ambiguous. The code panes let you inspect the actual hypotheses and bodies yourself.
Definitions (roots) is the default view. Definitions are roots and always show. A theorem is folded away only when it is proven (its Lean counterpart has no sorry and no proof-debt entry) and spot-checked by Claude against pinned Flocq, statement against statement. Every other theorem — unproved, unmatched, red, reviewed only by the port, or not yet checked — stays visible, and unproved theorems get a dashed red outline. A folded theorem’s dependency paths are compressed onto the nearest visible declarations it uses, which show a +n badge and list it in the inspector; each module also lists its folded theorems after its last page. Rocq-only declarations are neither roots nor open work: the roots view hides them too and lists them on the same strip under Rocq-only (n/a). All declarations shows the full graph.
sorry
A declaration is a theorem when Rocq compiles it as a proof of a proposition (dpdgraph’s prop flag), whatever its keyword. So Flocq’s Instances and Prop-valued Definitions count as theorems, and a Theorem that returns data, such as round_val_of_pred, counts as a definition.
prop
Instance
Definition
Theorem
round_val_of_pred
Green marks checked slices. Amber means a counterpart exists but is not marked reviewed here. White means no Lean counterpart; the port’s classification lists most as missing, with a port plan, and the inspector flags the rest: a classification entry whose Lean name is gone (stale), or a counterpart lost after the classification was written. Where this snapshot matches a classified declaration directly, the direct match sets its colour and the inspector flags the entry as superseded. Grey is Rocq-only: SProp eliminators (Lean has no SProp) and notations local to a Section (no compiled object) that the port’s classification finds nothing to port for; they are left out of progress ratios. Only declarations with no Lean match by name are classified, so an eliminator or notation whose name a Lean declaration reuses keeps that match’s colour. Blue is the current review slice. Red includes open proof obligations, which do not necessarily mean an algorithm is wrong, and renamed Lean declarations whose statement differs from Flocq’s.
This is a read-only snapshot, built separately from the port. Source matching and excerpt boundaries are intentionally approximate. It does not update automatically.