Cairn
lean/Cairn.lean
Cairn
What an app imports: import Cairn (in a module, public import Cairn). It brings in every
module of the Cairn library, the code bin/cairn-link links into an app (lakefile.lean): the
app model, layout, text, the runtime and its ABI (Cairn.Abi, Cairn.Runtime.Abi,
Cairn.Text.Host), effects, and the claim language, whose commands it meta-imports so they
run at compile time only (docs/claims.md, "Linking"). No proofs, no import Lean at run time.
The proofs, tests and tools are in other libraries, and CairnAll imports them all for the
ledger, the axiom audit and the docs. Keep this list to the Cairn library's roots: a module
outside it would make every app's link fail (bin/cairn-link warns).
Imports Cairn.Geometry, Cairn.Claim, Cairn.Effects, Cairn.Font, Cairn.Input, Cairn.UI.Node, Cairn.UI.Images, Cairn.UI.Grid, Cairn.UI.Hit, Cairn.Surface, Cairn.App, Cairn.VList, Cairn.Optimistic, Cairn.Claims.Move, Cairn.Claims.Machine, Cairn.Claims.Core, Cairn.Claims.Elab, Cairn.Text.Wrap, Cairn.Text.Field, Cairn.Text.Host, Cairn.Layout.Core, Cairn.Layout.Facts, Cairn.Runtime.World, Cairn.Runtime.Step, Cairn.Runtime.Abi, Cairn.Frame, Cairn.Frame.Bytes, Cairn.Frame.Encode, Cairn.Frame.Events, Cairn.Frame.Menu, Cairn.Frame.Build, Cairn.Abi, Cairn.Fuzz.Rng