Document specimen
A paragraph of running text, with inline code, a reference to the table part, and a status: proved. A line long enough to show the measure of a paragraph at the page's width. Its length can be judged against the type's size and the leading between lines.
Every statusstatuses
Each mark is a shape, with no hue (decisions row 354, point 2):
proved modulo goal open refuted absent assumed missing
- proved
- proved filled
- modulo
- modulo half
- goal
- goal hollow
- open
- open dashed
- refuted
- refuted the cross
Every block kindblocks
Fields, a list, and code in three languages.
- concept
reactive-scheduling- claim
- random-descent
- a field with a long label that wraps
- and a value that runs on for a while to wrap
- a first item
- a second item, with
code - a third item, with a status modulo
theorem complete_unique (eqv : Equivalence R) (bis : Bisim step R)
(dia : Diamond step R) : R t1 t2 ∧ c1.length = c2.length := by
exact ⟨hR, hl⟩Diagram source (Mermaid, 3 lines)
flowchart LR
A[edit] --> B[build]
B --> C[look]a plain text block
with its indentation keptA wide tabletables
| claim | role | status | pointer | a long column header |
|---|---|---|---|---|
random-descent | fundamentalProperty | proved | Effect4.Machine.Descent.complete_unique | a long cell that wraps |
keys-once | preservation | proved | Effect4.Run.session_keys_once | — |
schedule-independent | fundamentalProperty | absent | — | see the statuses |
A figurefigure
A graph as data, drawn by the view's layout. A node links to the part it opens, a goal is lit, and the figure is also given in words.
The figure in words
- decision_preserves modulo → loop_preserves, deliver_preserves
- loop_preserves modulo → countdown_parks
- deliver_preserves modulo, 2 steps → countdown_parks, frame_typing
- countdown_parks goal
- frame_typing proved
Nesting, level 2depth
Each part's heading level is its depth.
Level 3depth-3
Level 4depth-4
Level 5depth-5
Level 6depth-6
The deepest heading.