Documentation Verification Report

HasFresh

📁 Source: Cslib/Foundations/Data/HasFresh.lean

Statistics

Metric	Count
Definitions `FreeUnionConfig`, `finset`, `singleton`, `HasFresh`, `freeUnion`, `fresh`, `ofNatEmbed`, `ofSucc`, `of_infinite`, `elabFreeUnionConfig`, `freeUnion`, `instHasFreshFinsetOfDecidableEq`, `instHasFreshForallNat`, `instHasFreshInt`, `instHasFreshMultisetOfDecidableEqOfInhabited`, `instHasFreshNat`, `instHasFreshRat`	17
Theorems `fresh_exists`, `fresh_notMem`, `to_infinite`	3
Total	20

Cslib

Definitions

Name	Category	Theorems
`FreeUnionConfig` 📖	CompData	—
`HasFresh` 📖	CompData	—
`elabFreeUnionConfig` 📖	CompOp	—
`freeUnion` 📖	CompOp	—
`instHasFreshFinsetOfDecidableEq` 📖	CompOp	—
`instHasFreshForallNat` 📖	CompOp	—
`instHasFreshInt` 📖	CompOp	—
`instHasFreshMultisetOfDecidableEqOfInhabited` 📖	CompOp	—
`instHasFreshNat` 📖	CompOp	—
`instHasFreshRat` 📖	CompOp	—

Cslib.FreeUnionConfig

Definitions

Name	Category	Theorems
`finset` 📖	CompOp	—
`singleton` 📖	CompOp	—

Cslib.HasFresh

Definitions

Name	Category	Theorems
`freeUnion` 📖	CompOp	—
`fresh` 📖	CompOp	1 math math: `fresh_notMem`
`ofNatEmbed` 📖	CompOp	—
`ofSucc` 📖	CompOp	—
`of_infinite` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fresh_exists` 📖	—	—	—	—	`fresh_notMem`
`fresh_notMem` 📖	mathematical	—	`fresh`	—	—
`to_infinite` 📖	—	—	—	—	—

---

← Back to Index