Cairn Docs Claims Blog Packages

Claim ยท cairn 0.5.2

cairn^907 Carets follow the painted glyphs

An assumption of cairn 0.5.2.

Id
cairn^907
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, the caret offset after each grapheme is at or right of every glyph painted for the text before it.

Evidence

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

Where it's defined

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

Ledger

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