Basic

📁 Source: Batteries/Data/Nat/Basic.lean

Statistics

Metric	Count
Definitions casesDiagOn, ofBits, recAuxOn, recDiag, left, right, recDiagAux, recDiagOn, sqrt, iter, strongRec, strongRecMeasure	12
Theorems instNeZeroHPowOfNat_batteries	1
Total	13

Nat

Definitions

Name	Category	Theorems
casesDiagOn 📖	CompOp	4 math math: casesDiagOn_succ_succ, casesDiagOn_zero_succ, casesDiagOn_succ_zero, casesDiagOn_zero_zero
ofBits 📖	CompOp	12 math math: BitVec.toFin_ofFnLEAux, testBit_ofBits_ge, ofBits_testBit, BitVec.toNat_ofFnBE, BitVec.toNat_ofFnLEAux, Fin.val_ofBits, testBit_ofBits_lt, ofBits_lt_two_pow, BitVec.toNat_ofFnLE, ofBits_succ, testBit_ofBits, ofBits_zero
recAuxOn 📖	CompOp	2 math math: recAuxOn_succ, recAuxOn_zero
recDiag 📖	CompOp	4 math math: recDiag_succ_zero, recDiag_succ_succ, recDiag_zero_zero, recDiag_zero_succ
recDiagAux 📖	CompOp	3 math math: recDiagAux_zero_right, recDiagAux_zero_left, recDiagAux_succ_succ
recDiagOn 📖	CompOp	4 math math: recDiagOn_succ_zero, recDiagOn_zero_succ, recDiagOn_zero_zero, recDiagOn_succ_succ
sqrt 📖	CompOp	—
strongRec 📖	CompOp	1 math math: strongRec_eq
strongRecMeasure 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNeZeroHPowOfNat_batteries 📖	—	—	—	—	—

Nat.recDiag

Definitions

Name	Category	Theorems
left 📖	CompOp	—
right 📖	CompOp	—

Nat.sqrt

Definitions

Name	Category	Theorems
iter 📖	CompOp	—

---

← Back to Index