Documentation Verification Report

InferenceSystem

πŸ“ Source: Cslib/Foundations/Logic/InferenceSystem.lean

Statistics

MetricCount
DefinitionsInferenceSystem, Derivable, toDerivation, derivation, instCoeDerivableDerivation, instCoeDerivationDerivable, rwConclusion, Β«term⇓_Β»
8
TheoremsfromDerivation
1
Total9

Cslib.Logic

Definitions

NameCategoryTheorems
InferenceSystem πŸ“–CompDataβ€”

Cslib.Logic.InferenceSystem

Definitions

NameCategoryTheorems
Derivable πŸ“–MathDef
2 mathmath: Derivable.fromDerivation, Cslib.CLL.Proposition.instSymmDerivableMultisetConsTensor
derivation πŸ“–CompOpβ€”
instCoeDerivableDerivation πŸ“–CompOpβ€”
instCoeDerivationDerivable πŸ“–CompOpβ€”
rwConclusion πŸ“–CompOpβ€”
Β«term⇓_Β» πŸ“–CompOpβ€”

Cslib.Logic.InferenceSystem.Derivable

Definitions

NameCategoryTheorems
toDerivation πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
fromDerivation πŸ“–mathematicalβ€”Cslib.Logic.InferenceSystem.Derivableβ€”β€”

---

← Back to Index