2. Code Panels🔗

Definition2.1

Statement uses 1

Statement dependency previews

Preview

Definition 2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Docstring reference: a rendered premise n + 1. An automatic title follows: Definition 2.2.

Definition2.1

Statement uses 1

Statement dependency previews

Preview

Definition 2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Docstring reference: a rendered premise n + 1. An automatic title follows: Definition 2.2.

Lean code for Definition2.1●1 definition

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.docstringReferenceSourcePreviewRuntimeShowcase.CodePanelDecls.docstringReferenceSource : NatDocstring reference: a **rendered premise** $n + 1$.
An automatic title follows: `panel_docstring_target`.
 : NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

def PreviewRuntimeShowcase.CodePanelDecls.docstringReferenceSourcePreviewRuntimeShowcase.CodePanelDecls.docstringReferenceSource : NatDocstring reference: a **rendered premise** $n + 1$.
An automatic title follows: `panel_docstring_target`.
 :
  NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

Docstring reference: a rendered premise n + 1. An automatic title follows: panel_docstring_target.

Definition2.2

uses 0

Used by 1

Reverse dependency previews

Preview

Definition 2.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Lean code for Definition2.2●2 definitions

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.docstringReferenceTargetPreviewRuntimeShowcase.CodePanelDecls.docstringReferenceTarget : Nat : NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

def PreviewRuntimeShowcase.CodePanelDecls.docstringReferenceTargetPreviewRuntimeShowcase.CodePanelDecls.docstringReferenceTarget : Nat :
  NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.additionalCodeOnlyWitnessPreviewRuntimeShowcase.CodePanelDecls.additionalCodeOnlyWitness : Nat : NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

def PreviewRuntimeShowcase.CodePanelDecls.additionalCodeOnlyWitnessPreviewRuntimeShowcase.CodePanelDecls.additionalCodeOnlyWitness : Nat :
  NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

Definition2.3

uses 0used by 0✓L∃∀N

In-module external definition panel sample.

Lean code for Definition2.3●1 definition

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.previewExternalDefinition : Nat

def PreviewRuntimeShowcase.CodePanelDecls.previewExternalDefinition :
  Nat

Definition2.4

uses 0used by 0✓L∃∀N

Namespace-opened external definition panel sample.

Lean code for Definition2.4●1 definition

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.previewExternalDefinition : Nat

def PreviewRuntimeShowcase.CodePanelDecls.previewExternalDefinition :
  Nat

Definition2.5

uses 0used by 0✓L∃∀N

In-module external Lean abbrev panel sample. Status summaries stay definition-like, while the rendered declaration preserves the abbrev keyword.

Lean code for Definition2.5●1 definition

abbrevdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

abbrev PreviewRuntimeShowcase.CodePanelDecls.previewExternalAbbrev : Nat

abbrev PreviewRuntimeShowcase.CodePanelDecls.previewExternalAbbrev :
  Nat

Definition2.6

uses 0used by 0✓L∃∀N

In-module external unsafe definition panel sample.

Lean code for Definition2.6●1 definition

def(unsafe)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

unsafe def PreviewRuntimeShowcase.CodePanelDecls.previewExternalUnsafeDefinition :
  Nat

unsafe def PreviewRuntimeShowcase.CodePanelDecls.previewExternalUnsafeDefinition :
  Nat

Definition2.7

uses 0used by 0✓L∃∀N

External definition panel sample with multiple documented Lean definitions.

Lean code for Definition2.7●2 definitions

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedDefinition : Nat

def PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedDefinition :
  Nat

The first documented preview definition used to test multi-declaration
docstring rendering in external code panels.

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedFunction
  (n : Nat) : Nat

def PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedFunction
  (n : Nat) : Nat

Adds a small preview offset to `n`.

The second paragraph keeps paragraph spacing visible when several documented
definitions appear in the same code panel.

Theorem2.8

uses 0used by 0✓L∃∀N

In-module external theorem panel sample.

Lean code for Theorem2.8●1 theorem

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem :
  True

Theorem2.9

uses 0used by 0✓L∃∀N

External theorem panel sample with a declaration docstring.

Lean code for Theorem2.9●1 theorem

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedTheorem : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedTheorem :
  True

A documented preview theorem whose statement is intentionally small.

Theorem2.10

uses 0used by 0✓L∃∀N

In-module external theorem panel sample with multiple complete declarations.

Lean code for Theorem2.10●2 theorems

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem :
  True

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheoremTwo : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheoremTwo :
  True

Theorem2.11

uses 0used by 0⚠L∃∀N

In-module external theorem panel with a sorry-backed declaration.

Lean code for Theorem2.11●1 theorem, incomplete

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

contains sorry

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalSorry : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalSorry :
  True

Theorem2.12

uses 0used by 0⚠L∃∀N

In-module external theorem panel sample with mixed declaration health.

Lean code for Theorem2.12●2 theorems, 1 incomplete

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem :
  True

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

contains sorry

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalSorry : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalSorry :
  True

Theorem2.13

uses 0used by 0!L∃∀N

External theorem panel sample with multiple references and one missing declaration.

Lean code for Theorem2.13●2 declarations, 1 missing

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewExternalTheorem :
  True

PreviewRuntimeShowcase.CodePanelDecls.previewExternalMissingmissing declaration

declaration not found (name was not present during directive/code-block registration)

Definition2.14

uses 0used by 0✓L∃∀N

Out-of-module external definition panel sample.

Lean code for Definition2.14●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.

Theorem2.15

uses 0used by 0✓L∃∀N

Out-of-module external theorem panel sample.

Lean code for Theorem2.15●1 theorem

theoremdefined in Init/Data/Nat/Basic.lean

complete

theorem Nat.add_assoc (n m k : Nat) : n + m + k = n + (m + k)

theorem Nat.add_assoc (n m k : Nat) :
  n + m + k = n + (m + k)

Definition2.16

uses 0used by 0!L∃∀N

External declaration panel with a missing declaration.

Lean code for Definition2.16●1 declaration, 1 missing

PreviewRuntimeShowcase.CodePanelDecls.previewExternalMissingmissing declaration

declaration not found (name was not present during directive/code-block registration)

Theorem2.17

uses 0used by 0AL∃∀N

External theorem panel with an axiom-like declaration.

Lean code for Theorem2.17●1 definition, incomplete

axiomdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

axiom-like

axiom PreviewRuntimeShowcase.CodePanelDecls.previewExternalAxiom : True

axiom PreviewRuntimeShowcase.CodePanelDecls.previewExternalAxiom :
  True

Definition2.18

uses 0used by 0✓L∃∀N

External inductive panel sample with documented constructors.

Lean code for Definition2.18●1 definition

inductive(2 constructors)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

inductive PreviewRuntimeShowcase.CodePanelDecls.PreviewStage : Type

inductive PreviewRuntimeShowcase.CodePanelDecls.PreviewStage :
  Type

A small inductive type used to exercise rendered constructor lists.

Constructors

PreviewRuntimeShowcase.CodePanelDecls.PreviewStage.initial :
  PreviewStage

The initial stage of the preview workflow.

PreviewRuntimeShowcase.CodePanelDecls.PreviewStage.step
  (n : Nat) : PreviewStage

A numbered follow-up stage.

Definition2.19

uses 0used by 0✓L∃∀N

External class panel sample with documented methods.

Lean code for Definition2.19●1 definition

class(2 methods)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

class PreviewRuntimeShowcase.CodePanelDecls.PreviewFold (α : Type) : Type

class PreviewRuntimeShowcase.CodePanelDecls.PreviewFold
  (α : Type) : Type

A compact class used to exercise rendered method documentation.

Methods

neutral : α

The neutral preview value.

combine : α → α → α

Combine two preview values.

Definition2.20

uses 0used by 0✓L∃∀N

External structure panel sample with a field-heavy package shape.

Lean code for Definition2.20●1 definition

structure(6 fields)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

structure PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage : Type

structure PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage :
  Type

A preview Frey package is a compact stand-in for a structure whose constructor
duplicates a field-heavy mathematical record.

Fields

a : Nat

The first value in the package.

b : Nat

The second value in the package.

c : Nat

The target value in the package.

p : Nat

The prime-like exponent under discussion.

hp5 : 5 ≤ self.p

The lower-bound hypothesis on `p`.

hFLT : self.a ^ self.p + self.b ^ self.p = self.c ^ self.p

The Fermat-like equation carried by the package.

Theorem2.21

uses 0used by 0✓L∃∀N

External theorem panel sample with a Markdown-like docstring.

Lean code for Theorem2.21●1 theorem

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage.ofCounterexample
  {a b c p : Nat} (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) :
  Nonempty PreviewFreyPackage

theorem PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage.ofCounterexample
  {a b c p : Nat} (hp5 : 5 ≤ p)
  (H : a ^ p + b ^ p = c ^ p) :
  Nonempty PreviewFreyPackage

Given a counterexample `a^p + b^p = c^p` with `p >= 5`,
there exists a preview Frey package.

Definition2.22

uses 0used by 0✓L∃∀N

External declaration panel sample mixing definitions, theorems, inductives, classes, and structures.

Lean code for Definition2.22●5 declarations

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

def PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedDefinition : Nat

def PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedDefinition :
  Nat

The first documented preview definition used to test multi-declaration
docstring rendering in external code panels.

theoremdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

theorem PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedTheorem : True

theorem PreviewRuntimeShowcase.CodePanelDecls.previewDocstringedTheorem :
  True

A documented preview theorem whose statement is intentionally small.

inductive(2 constructors)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

inductive PreviewRuntimeShowcase.CodePanelDecls.PreviewStage : Type

inductive PreviewRuntimeShowcase.CodePanelDecls.PreviewStage :
  Type

A small inductive type used to exercise rendered constructor lists.

Constructors

PreviewRuntimeShowcase.CodePanelDecls.PreviewStage.initial :
  PreviewStage

The initial stage of the preview workflow.

PreviewRuntimeShowcase.CodePanelDecls.PreviewStage.step
  (n : Nat) : PreviewStage

A numbered follow-up stage.

class(2 methods)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

class PreviewRuntimeShowcase.CodePanelDecls.PreviewFold (α : Type) : Type

class PreviewRuntimeShowcase.CodePanelDecls.PreviewFold
  (α : Type) : Type

A compact class used to exercise rendered method documentation.

Methods

neutral : α

The neutral preview value.

combine : α → α → α

Combine two preview values.

structure(6 fields)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete

structure PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage : Type

structure PreviewRuntimeShowcase.CodePanelDecls.PreviewFreyPackage :
  Type

A preview Frey package is a compact stand-in for a structure whose constructor
duplicates a field-heavy mathematical record.

Fields

a : Nat

The first value in the package.

b : Nat

The second value in the package.

c : Nat

The target value in the package.

p : Nat

The prime-like exponent under discussion.

hp5 : 5 ≤ self.p

The lower-bound hypothesis on `p`.

hFLT : self.a ^ self.p + self.b ^ self.p = self.c ^ self.p

The Fermat-like equation carried by the package.

Definition2.23

uses 0used by 0✓L∃∀N

Inline code panel sample with complete Lean code.

Lean code for Definition2.23

def panelInlineOnlyOk : Nat := 0

Definition2.24

uses 0used by 0⚠L∃∀N

Inline code panel sample with a sorry-backed declaration.

Lean code for Definition2.24

theorem declaration uses `sorry`panelInlineOnlySorry : True := by⊢ True
  sorryAll goals completed! 🐙

Theorem2.25

uses 0used by 0✓L∃∀N

Inline code panel sample with multiple complete Lean theorems.

Lean code for Theorem2.25

theorem panelInlineMultiTheoremOkLeft : True := by⊢ True
  trivialAll goals completed! 🐙

theorem panelInlineMultiTheoremOkRight : True := by⊢ True
  trivialAll goals completed! 🐙

Theorem2.26

uses 0used by 0⚠L∃∀N

Inline code panel sample with multiple Lean theorems and mixed declaration health.

Lean code for Theorem2.26

theorem panelInlineMultiTheoremWarningOk : True := by⊢ True
  trivialAll goals completed! 🐙

theorem declaration uses `sorry`panelInlineMultiTheoremWarningSorry : True := by⊢ True
  sorryAll goals completed! 🐙

Definition2.27

uses 0used by 0⚠L∃∀N

Inline code panel sample with mixed declaration health.

Lean code for Definition2.27

def panelInlineOk : Nat := 0

theorem declaration uses `sorry`panelInlineSorry : True := by⊢ True
  sorryAll goals completed! 🐙

Definition2.28

uses 0used by 0AL∃∀N

Inline code panel sample with an axiom-like declaration.

Lean code for Definition2.28

axiom panelInlineAxiom : True

Definition2.29

uses 0used by 0✓L∃∀N

Inline Lean structure sample with declaration and field docstrings.

Lean code for Definition2.29

/--
Inline package docstring used to compare literate Lean
against the external declaration renderer.

* The field `left` is shown as inline code.
* **Bold text** checks richer Markdown.
-/
structure PanelInlineDocstringedStructure where
  /-- The left inline field. -/
  left : Nat
  /-- The right inline field. -/
  right : Nat
  /--
  A proof-like field that keeps dependent-looking field
  layout visible.
  -/
  ordered : left <= right

Definition2.30

uses 0used by 0✓L∃∀N

Inline Lean inductive sample with declaration and constructor docstrings.

Lean code for Definition2.30

/--
Inline workflow stage docstring used to compare
constructor documentation.
-/
inductive PanelInlineDocstringedStage where
  /-- The initial inline stage. -/
  | initial
  /-- A follow-up inline stage carrying a counter. -/
  | followup (_ : Nat)

Definition2.31

uses 0used by 0✓L∃∀N

Inline Lean panel sample mixing documented structures, inductives, and classes.

Lean code for Definition2.31

/-- Inline mixed configuration docstring. -/
structure PanelInlineMixedConfig where
  /-- Whether the preview branch is enabled. -/
  enabled : Bool

/-- Inline mixed state docstring. -/
inductive PanelInlineMixedState where
  /-- The ready state. -/
  | ready
  /-- The running state with a step count. -/
  | running (_ : Nat)

/-- Inline mixed fold class docstring. -/
class PanelInlineMixedFold (α : Type) where
  /-- The empty inline value. -/
  empty : α
  /-- Merge two inline values. -/
  merge : α -> α -> α

Definition2.32

uses 0used by 0XL∃∀N

Statement without associated Lean code.

Definition2.33

uses 0used by 0✓L∃∀N

External definition panel sample with a structural Verso docstring.

Lean code for Definition2.33●1 definition

defdefined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete
def PreviewRuntimeShowcase.CodePanelDecls.previewVersoDocstringedDefinition : Nat
def PreviewRuntimeShowcase.CodePanelDecls.previewVersoDocstringedDefinition : Nat
A structural external-panel docstring with inline mathematics 6 + 1 = 7.

A display equation follows: 6 + 2 = 8

First structural panel item.

Second structural panel item.

Definition2.34

uses 0used by 0✓L∃∀N

External structure panel sample with structural declaration and field docstrings.

Lean code for Definition2.34●1 definition

structure(1 field)defined in PreviewRuntimeShowcase/Chapters/CodePanels.lean

complete
structure PreviewRuntimeShowcase.CodePanelDecls.PreviewVersoDocstringedStructure : Type
structure PreviewRuntimeShowcase.CodePanelDecls.PreviewVersoDocstringedStructure : Type
A structural container docstring for a field-docstring regression.
Fields

value : Nat

A structural field docstring with inline mathematics 8 + 1 = 9.