Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^990 Wrapped lines paint as wide as Lean measured them

An assumption of cairn 0.5.2.

Id
cairn^990
Kind
assume
Reads as
assumed
Version
0.5.2

All of cairn 0.5.2's claims

What it says

On left-to-right text without controls or tabs, each line Lean's wrapping chose, shaped again on its own by the host, is within 1 + ceil(0.15 em) points of the width Lean took from the whole string's carets, and so fits the width up to that slack; laid lines sit at x 0, one line height apart.

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the trusted-base fuzzer's check text.wrap.painted held. A CI step will publish it (#95).

Where it's defined

Declaration
Cairn.Fuzz.Trusted.Claims.wrapPainted
Module
Cairn.Fuzz.Trusted.Claims
Source
lean/Cairn/Fuzz/Trusted/Claims.lean:146 at v0.5.2
Statement hash
-

Ledger

cairn^990 is active in this version's claims.lock. An id never moves or changes meaning.