External Markup Source Showcase

3. Selected Markdown preview with TeX alongside🔗

When a bodyless node has more than one source witness, the generator must choose one witness for the rendered preview body. This example carries both Markdown and TeX statement witnesses. The default render preference chooses Markdown for the preview body, while the header badges still show that both source formats are attached.

Theorem3.1
Original source
Source provenance preview
Preview
Original source
  • Documentimported-paper
    imported-paper p. 12
    • page 12; text source/pages/page-12.md:16-26; pdf source/pages/page-12.pdf; image source/pages/images/page-12.png
uses 0used by 0markupMDmarkupTeX✓L∃∀N
Tagsexternal-sourcemixed-markupselected-markdownbodyless

Rendered from external Markdown source (statement): source/pages/page-12.md:16:0-26:0; no native Verso body is available.

Selected Markdown statement

This Markdown witness is selected for the rendered preview body even though a TeX statement witness is attached to the same node.

Lean code for Theorem3.1●1 definition
  • defdefined in Init/Prelude.lean
    complete
    def Nat.add : Nat → Nat → Nat
    def Nat.add : Nat → Nat → Nat
    Addition of natural numbers, typically used via the `+` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.