External Markup Source Showcase🔗

This showcase models a Blueprint that is being migrated from an imported paper. The visible text is the current informal Blueprint layer. The MD and TeX badges in Blueprint headers mark original source markup that is attached to the same label, even when that source is not shown inline.

There are three layers in play:

• the original source pages and extracted markup;

• the informal Blueprint node, which may already be native Verso or may still be bodyless;

• the Lean declarations attached with (lean := ...).