Cairn.Font
lean/Cairn/Font.lean
Text metrics: the one place layout depends on the host.
Layout is parameterised by a TextMetrics. Theorems quantify over every metrics that is
Valid; at run time the host supplies Core Text's (an assume claim, checked by logging and
replay). Text indices are Unicode scalar positions (String.length), not bytes and not UTF-16.
Grapheme clusters are not modelled in M1. A metrics measures one line; wrapped text
(Node.para) is broken into lines by Lean from one measurement of the whole string
(Cairn.Text.Wrap).
Imports Cairn.Geometry
Structures 3
Font : Type
family : Nat0 is the system UI font, 1 the system monospaced font.
size : NatPoints.
weight : Nat100–900, CSS-style.
italic : Boolwidth : FontWidth
tracking : IntExtra space after every character, in hundredths of a point (SwiftUI's tracking):
140 is 1.4 pt. Measured and painted alike.
tabular : BoolDigits all one width (SwiftUI's monospacedDigit), so a clock doesn't jitter.
TextMetrics : Type
offsets : Array IntCaret offsets: entry i is the x offset of the boundary before scalar i, so the array
has s.length + 1 entries, starts at 0 and never decreases. The last entry is the width.
ascent : Intdescent : IntValid (m : TextMetrics) : Prop
What every metrics must satisfy. Layout and text theorems assume this and nothing more.
size : (m.offsets f s).size = s.length + 1
zero : (m.offsets f s)[0]? = some 0
mono : (m.offsets f s)[i] ≤ (m.offsets f s)[j]
ascent : 0 ≤ m.ascent f
descent : 0 ≤ m.descent f
Inductive types 1
FontWidth : Type
A font's width axis: SwiftUI's Font.Width presets, which the system font's variable width
axis implements (NSFont.Width: standard 0, condensed −0.2, expanded 0.2, compressed −0.4).
Definitions 5
code : FontWidth → Nat
The width's code on the wire and in the metrics ABI.
ofCode? : Nat → Option FontWidth
width (m : TextMetrics) (f : Font) (s : String) : Int
lineHeight (m : TextMetrics) (f : Font) : Int
mono : TextMetrics
A deterministic stand-in for tests and examples: every scalar is size * 6 / 10 wide.
Theorems 2
ofCode_code (w : FontWidth) : ofCode? w.code = some w
code_lt (w : FontWidth) : w.code < 4
Instances 10
instDecidableEqFontWidth : DecidableEq FontWidth
instBEqFontWidth : BEq FontWidth
instHashableFontWidth : Hashable FontWidth
instReprFontWidth : Repr FontWidth
instInhabitedFontWidth : Inhabited FontWidth
instInhabitedFont : Inhabited Font
instReprFont : Repr Font
instDecidableEqFont : DecidableEq Font
instHashableFont : Hashable Font
instBEqFont : BEq Font