Basic

📁 Source: Mathlib/Data/String/Basic.lean

Statistics

Metric	Count
Definitions LE, LT', decidableLE, decidableLT', instLinearOrder, ltb, inductionOn	7
Theorems asString_eq, toList_asString, asString_nil, asString_toList, head_empty, le_iff_toList_le, lt_iff_toList_lt, ltb_cons_addChar, ltb_cons_addChar', ofList_eq, toList_nonempty	11
Total	18

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asString_eq 📖	—	—	—	—	String.ofList_eq
toList_asString 📖	—	—	—	—	—

String

Definitions

Name	Category	Theorems
LE 📖	CompOp	1 math math: le_iff_toList_le
LT' 📖	CompOp	1 math math: lt_iff_toList_lt
decidableLE 📖	CompOp	—
decidableLT' 📖	CompOp	—
instLinearOrder 📖	CompOp	—
ltb 📖	CompOp	2 math math: ltb_cons_addChar, ltb_cons_addChar'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asString_nil 📖	—	—	—	—	—
asString_toList 📖	—	—	—	—	—
head_empty 📖	—	—	—	—	—
le_iff_toList_le 📖	mathematical	—	LE List.LE' instLinearOrderChar	—	lt_iff_toList_lt not_lt
lt_iff_toList_lt 📖	mathematical	—	LT'	—	ltb.eq_def Nat.instCanonicallyOrderedAdd not_lt_of_gt ltb_cons_addChar List.lex_cons_iff
ltb_cons_addChar 📖	mathematical	—	ltb	—	ltb_cons_addChar'
ltb_cons_addChar' 📖	mathematical	—	ltb	—	ltb.induct_unfolding ltb.eq_1
ofList_eq 📖	—	—	—	—	—
toList_nonempty 📖	—	—	—	—	—

String.ltb

Definitions

Name	Category	Theorems
inductionOn 📖	CompOp	—

---

← Back to Index