Cairn
Docs
Claims
Blog
Packages
Claim ยท cairn 0.4.1
cairn^906 The host's text metrics are what layout assumes
An assumption of cairn 0.4.1.
- Id
cairn^906- Kind
- assume
- Reads as
- assumed
- Version
- 0.4.1
What it says
cairn_text_metrics gives one offset per scalar boundary, from 0 and nondecreasing, with nonnegative ascent and descent, and Lean's TextMetrics.host sees those numbers unchanged.
Evidence
| assumed | Stated, not proved. The proofs rely on it. | |
| fuzzed | Not shown yet: the trusted-base fuzzer's check text.metrics held. A CI step will publish it (#95). | |
Where it's defined
- Declaration
Cairn.Fuzz.Trusted.Claims.textMetricsHost- Module
Cairn.Fuzz.Trusted.Claims- Source
lean/Cairn/Fuzz/Trusted/Claims.lean:36atv0.4.1- Statement hash
-
Ledger
cairn^906 is active in this version's claims.lock. An id never moves or changes meaning.