Basic

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

Statistics

Metric	Count
Definitions Proof, ax', bot_inversion, cut', parr_inversion, rwConclusion, with_inversion₁, with_inversion₂, Proposition, fill, Equiv, bang_top_eqv_one, dual, equiv, refl, symm, trans, instBEqContext, beq, instDecidableEqContext, decEq, instLogicalEquivalenceSequentProof, linImpl, negative, negative_decidable, oplus_idem, parr_top_eqv_top, positive, positive_decidable, propositionSetoid, quest_zero_eqv_bot, subst_eqv, subst_eqv_head, tensor_assoc, tensor_distrib_oplus, tensor_symm, tensor_zero_eqv_zero, with_idem, Sequent, fill, allQuest, chooseEquiv, instBEqProposition, beq, instBotProposition, instCoeEquivEquiv, instDecidableEqProposition, decEq, instHasContextProposition, instHasHContextSequentProposition, instInferenceSystemSequent, instOneProposition, instTopProposition, instZeroProposition, term!_, term_⅋_, «term_&_», «term_≡_», «term_≡⇓_», «term_⊕_», «term_⊗_», «term_⊸_», «term_⫠», «termʔ_»	64
Theorems refl, symm, trans, add_middle_eq_cons, context_fill_def, dual_inj, dual_involution, dual_neq, dual_sizeOf, toProp, instCongruenceEquiv, instIsEquivEquiv, instSymmDerivableMultisetConsTensor, top_eq_zero_dual	14
Total	78

Cslib.CLL

Definitions

Name	Category	Theorems
Proof 📖	CompData	—
Proposition 📖	CompData	7 math, 1 bridge math: Proposition.add_middle_eq_cons, Proposition.dual_sizeOf, Proposition.instCongruenceEquiv, Proposition.instIsEquivEquiv, Proposition.top_eq_zero_dual, Proposition.context_fill_def, Proposition.instSymmDerivableMultisetConsTensor bridge: Proof.expand_onlyAtomicAxioms
Sequent 📖	CompOp	1 bridge bridge: Proof.expand_onlyAtomicAxioms
chooseEquiv 📖	CompOp	—
instBEqProposition 📖	CompOp	—
instBotProposition 📖	CompOp	—
instCoeEquivEquiv 📖	CompOp	—
instDecidableEqProposition 📖	CompOp	—
instHasContextProposition 📖	CompOp	2 math math: Proposition.instCongruenceEquiv, Proposition.context_fill_def
instHasHContextSequentProposition 📖	CompOp	—
instInferenceSystemSequent 📖	CompOp	1 math math: Proposition.instSymmDerivableMultisetConsTensor
instOneProposition 📖	CompOp	—
instTopProposition 📖	CompOp	1 math math: Proposition.top_eq_zero_dual
instZeroProposition 📖	CompOp	1 math math: Proposition.top_eq_zero_dual
term!_ 📖	CompOp	—
term_⅋_ 📖	CompOp	—
«term_&_» 📖	CompOp	—
«term_≡_» 📖	CompOp	—
«term_≡⇓_» 📖	CompOp	—
«term_⊕_» 📖	CompOp	—
«term_⊗_» 📖	CompOp	—
«term_⊸_» 📖	CompOp	—
«term_⫠» 📖	CompOp	—
«termʔ_» 📖	CompOp	—

Cslib.CLL.Proof

Definitions

Name	Category	Theorems
ax' 📖	CompOp	—
bot_inversion 📖	CompOp	—
cut' 📖	CompOp	—
parr_inversion 📖	CompOp	—
rwConclusion 📖	CompOp	1 bridge bridge: onlyAtomicAxioms_rwConclusion
with_inversion₁ 📖	CompOp	—
with_inversion₂ 📖	CompOp	—

Cslib.CLL.Proposition

Definitions

Name	Category	Theorems
Equiv 📖	MathDef	6 math math: Equiv.refl, Equiv.trans, Equiv.symm, instCongruenceEquiv, instIsEquivEquiv, equiv.toProp
bang_top_eqv_one 📖	CompOp	—
dual 📖	CompOp	4 math, 1 bridge math: dual_involution, dual_inj, dual_sizeOf, top_eq_zero_dual bridge: Cslib.CLL.Proof.expand_onlyAtomicAxioms
equiv 📖	CompOp	—
instBEqContext 📖	CompOp	—
instDecidableEqContext 📖	CompOp	—
instLogicalEquivalenceSequentProof 📖	CompOp	—
linImpl 📖	CompOp	—
negative 📖	CompOp	—
negative_decidable 📖	CompOp	—
oplus_idem 📖	CompOp	—
parr_top_eqv_top 📖	CompOp	—
positive 📖	CompOp	—
positive_decidable 📖	CompOp	—
propositionSetoid 📖	CompOp	—
quest_zero_eqv_bot 📖	CompOp	—
subst_eqv 📖	CompOp	—
subst_eqv_head 📖	CompOp	—
tensor_assoc 📖	CompOp	—
tensor_distrib_oplus 📖	CompOp	—
tensor_symm 📖	CompOp	—
tensor_zero_eqv_zero 📖	CompOp	—
with_idem 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_middle_eq_cons 📖	mathematical	—	Cslib.CLL.Proposition	—	—
context_fill_def 📖	mathematical	—	Cslib.HasHContext.fill Cslib.CLL.Proposition Cslib.CLL.instHasContextProposition Context.fill	—	—
dual_inj 📖	mathematical	—	dual	—	—
dual_involution 📖	mathematical	—	dual	—	—
dual_neq 📖	—	—	—	—	—
dual_sizeOf 📖	mathematical	—	Cslib.CLL.Proposition dual	—	—
instCongruenceEquiv 📖	mathematical	—	Cslib.Congruence Cslib.CLL.Proposition Cslib.CLL.instHasContextProposition Equiv	—	instIsEquivEquiv
instIsEquivEquiv 📖	mathematical	—	Cslib.CLL.Proposition Equiv	—	Equiv.refl Equiv.trans Equiv.symm
instSymmDerivableMultisetConsTensor 📖	mathematical	—	Cslib.CLL.Proposition Cslib.Logic.InferenceSystem.Derivable Cslib.CLL.instInferenceSystemSequent tensor	—	Cslib.Logic.InferenceSystem.Derivable.fromDerivation
top_eq_zero_dual 📖	mathematical	—	Cslib.CLL.Proposition Cslib.CLL.instTopProposition dual Cslib.CLL.instZeroProposition	—	—

Cslib.CLL.Proposition.Context

Definitions

Name	Category	Theorems
fill 📖	CompOp	1 math math: Cslib.CLL.Proposition.context_fill_def

Cslib.CLL.Proposition.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	mathematical	—	Cslib.CLL.Proposition.Equiv	—	Cslib.CLL.Proposition.equiv.toProp
symm 📖	mathematical	Cslib.CLL.Proposition.Equiv	Cslib.CLL.Proposition.Equiv	—	—
trans 📖	mathematical	Cslib.CLL.Proposition.Equiv	Cslib.CLL.Proposition.Equiv	—	Cslib.CLL.Proposition.equiv.toProp

Cslib.CLL.Proposition.equiv

Definitions

Name	Category	Theorems
refl 📖	CompOp	—
symm 📖	CompOp	—
trans 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toProp 📖	mathematical	—	Cslib.CLL.Proposition.Equiv	—	Cslib.Logic.InferenceSystem.Derivable.fromDerivation

Cslib.CLL.Proposition.instBEqContext

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Cslib.CLL.Proposition.instDecidableEqContext

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

Cslib.CLL.Sequent

Definitions

Name	Category	Theorems
allQuest 📖	CompOp	—

Cslib.CLL.Sequent.Context

Definitions

Name	Category	Theorems
fill 📖	CompOp	—

Cslib.CLL.instBEqProposition

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Cslib.CLL.instDecidableEqProposition

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index