Documentation Verification Report

UInt

📁 Source: Batteries/Data/UInt.lean

Statistics

Metric	Count
Definitions	0
Theorems `compare_eq_toNat_compare_toNat`, `ext`, `ext_iff`, `le_iff_toNat_le_toNat`, `lt_iff_toNat_lt_toNat`, `max_def`, `min_def`, `toNat_max`, `toNat_min`, `toUInt32_toNat`, `toUInt64_toNat`, `toUInt8_toNat`, `compare_eq_toNat_compare_toNat`, `ext`, `ext_iff`, `le_iff_toNat_le_toNat`, `lt_iff_toNat_lt_toNat`, `max_def`, `min_def`, `toNat_max`, `toNat_min`, `toUInt16_toNat`, `toUInt64_toNat`, `toUInt8_toNat`, `toUSize_toNat`, `compare_eq_toNat_compare_toNat`, `ext`, `ext_iff`, `le_iff_toNat_le_toNat`, `lt_iff_toNat_lt_toNat`, `max_def`, `min_def`, `toNat_max`, `toNat_min`, `toUInt16_toNat`, `toUInt32_toNat`, `toUInt8_toNat`, `compare_eq_toNat_compare_toNat`, `ext`, `ext_iff`, `le_iff_toNat_le_toNat`, `lt_iff_toNat_lt_toNat`, `max_def`, `min_def`, `toNat_max`, `toNat_min`, `toUInt16_toNat`, `toUInt32_toNat`, `toUInt64_toNat`, `ext`, `ext_iff`, `pred_toNat`, `toNat_ofNat_of_le_of_lt`, `toUInt64_toNat`, `instLawfulOrdUInt16`, `instLawfulOrdUInt32`, `instLawfulOrdUInt64`, `instLawfulOrdUInt8`, `instLawfulOrdUSize`	59
Total	59

UInt16

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_eq_toNat_compare_toNat` 📖	—	—	—	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`le_iff_toNat_le_toNat` 📖	—	—	—	—	—
`lt_iff_toNat_lt_toNat` 📖	—	—	—	—	—
`max_def` 📖	—	—	—	—	—
`min_def` 📖	—	—	—	—	—
`toNat_max` 📖	—	—	—	—	`max_def` `le_iff_toNat_le_toNat`
`toNat_min` 📖	—	—	—	—	`min_def` `le_iff_toNat_le_toNat`
`toUInt32_toNat` 📖	—	—	—	—	—
`toUInt64_toNat` 📖	—	—	—	—	—
`toUInt8_toNat` 📖	—	—	—	—	—

UInt32

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_eq_toNat_compare_toNat` 📖	—	—	—	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`le_iff_toNat_le_toNat` 📖	—	—	—	—	—
`lt_iff_toNat_lt_toNat` 📖	—	—	—	—	—
`max_def` 📖	—	—	—	—	—
`min_def` 📖	—	—	—	—	—
`toNat_max` 📖	—	—	—	—	`max_def` `le_iff_toNat_le_toNat`
`toNat_min` 📖	—	—	—	—	`min_def` `le_iff_toNat_le_toNat`
`toUInt16_toNat` 📖	—	—	—	—	—
`toUInt64_toNat` 📖	—	—	—	—	—
`toUInt8_toNat` 📖	—	—	—	—	—
`toUSize_toNat` 📖	—	—	—	—	—

UInt64

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_eq_toNat_compare_toNat` 📖	—	—	—	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`le_iff_toNat_le_toNat` 📖	—	—	—	—	—
`lt_iff_toNat_lt_toNat` 📖	—	—	—	—	—
`max_def` 📖	—	—	—	—	—
`min_def` 📖	—	—	—	—	—
`toNat_max` 📖	—	—	—	—	`max_def` `le_iff_toNat_le_toNat`
`toNat_min` 📖	—	—	—	—	`min_def` `le_iff_toNat_le_toNat`
`toUInt16_toNat` 📖	—	—	—	—	—
`toUInt32_toNat` 📖	—	—	—	—	—
`toUInt8_toNat` 📖	—	—	—	—	—

UInt8

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_eq_toNat_compare_toNat` 📖	—	—	—	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`le_iff_toNat_le_toNat` 📖	—	—	—	—	—
`lt_iff_toNat_lt_toNat` 📖	—	—	—	—	—
`max_def` 📖	—	—	—	—	—
`min_def` 📖	—	—	—	—	—
`toNat_max` 📖	—	—	—	—	`max_def` `le_iff_toNat_le_toNat`
`toNat_min` 📖	—	—	—	—	`min_def` `le_iff_toNat_le_toNat`
`toUInt16_toNat` 📖	—	—	—	—	—
`toUInt32_toNat` 📖	—	—	—	—	—
`toUInt64_toNat` 📖	—	—	—	—	—

USize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`pred_toNat` 📖	—	—	—	—	—
`toNat_ofNat_of_le_of_lt` 📖	—	—	—	—	—
`toUInt64_toNat` 📖	—	—	—	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLawfulOrdUInt16` 📖	mathematical	—	`Std.LawfulOrd`	—	`Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`instLawfulOrdUInt32` 📖	mathematical	—	`Std.LawfulOrd`	—	`Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`instLawfulOrdUInt64` 📖	mathematical	—	`Std.LawfulOrd`	—	`Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`instLawfulOrdUInt8` 📖	mathematical	—	`Std.LawfulOrd`	—	`Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`instLawfulOrdUSize` 📖	mathematical	—	`Std.LawfulOrd`	—	`Std.LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`

---

← Back to Index