EtaExpansion

📁 Source: Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean

Statistics

Metric	Count
Definitions onlyAtomicAxioms, expand	2
Theorems expand_onlyAtomicAxioms, onlyAtomicAxioms_rwConclusion	2
Total	4

Cslib.CLL.Proof

Definitions

Name	Category	Theorems
onlyAtomicAxioms 📖	CompOp	1 bridge bridge: expand_onlyAtomicAxioms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expand_onlyAtomicAxioms 📖	bridging (complete)	—	onlyAtomicAxioms Cslib.CLL.Proposition Cslib.CLL.Sequent Cslib.CLL.Proposition.dual Cslib.CLL.Proposition.expand	onlyAtomicAxioms	—
onlyAtomicAxioms_rwConclusion 📖	bridging (sound)	onlyAtomicAxioms	rwConclusion	onlyAtomicAxioms	—

Cslib.CLL.Proposition

Definitions

Name	Category	Theorems
expand 📖	CompOp	1 bridge bridge: Cslib.CLL.Proof.expand_onlyAtomicAxioms

---

← Back to Index