Preview Runtime Showcase

4.1. Nested External Declaration Panels🔗

Issue #130 heading-outline reproduction.

These Blueprint nodes live on a nested Manual page so the generated page has real surrounding headings. The external declaration subsection labels below should be visible without entering the page heading outline.

Definition4.1.1
uses 0used by 0✓L∃∀N

Structure panel that renders the Fields label inside the declaration body.

Lean code for Definition4.1.1●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.
Definition4.1.2
uses 0used by 0✓L∃∀N

Class panel that renders the Methods label inside the declaration body.

Lean code for Definition4.1.2●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.
Definition4.1.3
uses 0used by 0✓L∃∀N

Inductive panel that renders the Constructors label inside the declaration body.

Lean code for Definition4.1.3●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 :
  PreviewRuntimeShowcase.CodePanelDecls.PreviewStage
    The initial stage of the preview workflow. 
    PreviewRuntimeShowcase.CodePanelDecls.PreviewStage.step
  (n : Nat) :
  PreviewRuntimeShowcase.CodePanelDecls.PreviewStage
    A numbered follow-up stage.
Definition4.1.4
uses 0used by 0✓L∃∀N

Extending structure panel that renders the Extends label inside the declaration body.

Lean code for Definition4.1.4●1 definition
  • structure(extends 1, 2 fields)defined in PreviewRuntimeShowcase/Chapters/ExternalDeclHeadings/Nested.lean
    complete
    structure PreviewRuntimeShowcase.ExternalDeclHeadingDecls.HeadingExtends : Type
    structure PreviewRuntimeShowcase.ExternalDeclHeadingDecls.HeadingExtends :
  Type
    An extending structure used to exercise the `Extends` subsection label.

    Extends

    • PreviewRuntimeShowcase.ExternalDeclHeadingDecls.HeadingBase

    Fields

    base : Nat
    Inherited from
    1. PreviewRuntimeShowcase.ExternalDeclHeadingDecls.HeadingBase
    extra : Nat
    A field owned by the extending structure.