LogicalEquivalence

📁 Source: Cslib/Logics/HML/LogicalEquivalence.lean

Statistics

Metric	Count
Definitions fill, Equiv, Bundled, fill, lts, state, Judgement, lts, state, φ, instHasContextProposition, instLogicalEquivalencePropositionJudgementBundled, judgementalContext	13
Theorems equiv_def, bundled_char, instCongruencePropositionEquiv, instIsEquivPropositionEquiv	4
Total	17

Cslib.Logic.HML

Definitions

Name	Category	Theorems
instHasContextProposition 📖	CompOp	1 math math: instCongruencePropositionEquiv
instLogicalEquivalencePropositionJudgementBundled 📖	CompOp	—
judgementalContext 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCongruencePropositionEquiv 📖	mathematical	—	Cslib.Congruence Proposition instHasContextProposition Proposition.Equiv	—	instIsEquivPropositionEquiv
instIsEquivPropositionEquiv 📖	mathematical	—	Proposition Proposition.Equiv	—	—

Cslib.Logic.HML.Proposition

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	3 math math: Cslib.Logic.HML.instCongruencePropositionEquiv, Cslib.Logic.HML.instIsEquivPropositionEquiv, equiv_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_def 📖	mathematical	—	Equiv denotation	—	—

Cslib.Logic.HML.Proposition.Context

Definitions

Name	Category	Theorems
fill 📖	CompOp	—

Cslib.Logic.HML.Satisfies

Definitions

Name	Category	Theorems
Bundled 📖	MathDef	1 math math: bundled_char
Judgement 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bundled_char 📖	mathematical	—	Bundled Cslib.Logic.HML.Satisfies Judgement.lts Judgement.state Judgement.φ	—	—

Cslib.Logic.HML.Satisfies.Context

Definitions

Name	Category	Theorems
fill 📖	CompOp	—
lts 📖	CompOp	—
state 📖	CompOp	—

Cslib.Logic.HML.Satisfies.Judgement

Definitions

Name	Category	Theorems
lts 📖	CompOp	1 math math: Cslib.Logic.HML.Satisfies.bundled_char
state 📖	CompOp	1 math math: Cslib.Logic.HML.Satisfies.bundled_char
φ 📖	CompOp	1 math math: Cslib.Logic.HML.Satisfies.bundled_char

---

← Back to Index