Documentation Verification Report

Modules

93 modules

ModuleDefinitionsTheoremsSorry
Cslib/Algorithms/Lean/MergeSort/MergeSort.lean 6 15
Cslib/Algorithms/Lean/TimeM.lean 10 17
Cslib/Computability/Automata/Acceptors/Acceptor.lean 3 1
Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean 3 1
Cslib/Computability/Automata/DA/Basic.lean 16 3
Cslib/Computability/Automata/DA/Buchi.lean 2 1
Cslib/Computability/Automata/DA/Congr.lean 1 2
Cslib/Computability/Automata/DA/Prod.lean 1 1
Cslib/Computability/Automata/DA/ToNA.lean 4 3
Cslib/Computability/Automata/EpsilonNA/Basic.lean 8 0
Cslib/Computability/Automata/EpsilonNA/ToNA.lean 2 2
Cslib/Computability/Automata/NA/Basic.lean 15 2
Cslib/Computability/Automata/NA/BuchiEquiv.lean 1 3
Cslib/Computability/Automata/NA/BuchiInter.lean 5 3
Cslib/Computability/Automata/NA/Concat.lean 2 9
Cslib/Computability/Automata/NA/Hist.lean 2 2
Cslib/Computability/Automata/NA/Loop.lean 2 11
Cslib/Computability/Automata/NA/Pair.lean 3 10
Cslib/Computability/Automata/NA/Prod.lean 1 1
Cslib/Computability/Automata/NA/Sum.lean 1 2
Cslib/Computability/Automata/NA/ToDA.lean 2 1
Cslib/Computability/Automata/NA/Total.lean 2 3
Cslib/Computability/Languages/Congruences/BuchiCongruence.lean 2 2
Cslib/Computability/Languages/Congruences/RightCongruence.lean 3 1
Cslib/Computability/Languages/ExampleEventuallyZero.lean 2 2
Cslib/Computability/Languages/Language.lean 0 10
Cslib/Computability/Languages/OmegaLanguage.lean 19 56
Cslib/Computability/Languages/OmegaRegularLanguage.lean 1 15
Cslib/Computability/Languages/RegularLanguage.lean 0 13
Cslib/Computability/URM/Basic.lean 5 20
Cslib/Computability/URM/Computable.lean 2 0
Cslib/Computability/URM/Defs.lean 28 0
Cslib/Computability/URM/Execution.lean 12 13
Cslib/Computability/URM/StandardForm.lean 3 15
Cslib/Computability/URM/StraightLine.lean 4 9
Cslib/Foundations/Control/Monad/Free.lean 10 23
Cslib/Foundations/Control/Monad/Free/Effects.lean 33 31
Cslib/Foundations/Control/Monad/Free/Fold.lean 1 3
Cslib/Foundations/Data/FinFun.lean 7 16
Cslib/Foundations/Data/HasFresh.lean 17 3
Cslib/Foundations/Data/Nat/Segment.lean 2 19
Cslib/Foundations/Data/OmegaSequence/Defs.lean 17 0
Cslib/Foundations/Data/OmegaSequence/Flatten.lean 3 17
Cslib/Foundations/Data/OmegaSequence/InfOcc.lean 1 2
Cslib/Foundations/Data/OmegaSequence/Init.lean 1 107
Cslib/Foundations/Data/OmegaSequence/Temporal.lean 2 9
Cslib/Foundations/Data/RelatesInSteps.lean 2 23
Cslib/Foundations/Data/Relation.lean 22 50
Cslib/Foundations/Data/Set/Saturation.lean 1 2
Cslib/Foundations/Lint/Basic.lean 1 0
Cslib/Foundations/Semantics/FLTS/Basic.lean 3 2
Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean 3 3
Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean 1 3
Cslib/Foundations/Semantics/FLTS/Prod.lean 1 1
Cslib/Foundations/Semantics/LTS/Basic.lean 49 55
Cslib/Foundations/Semantics/LTS/Bisimulation.lean 12 41
Cslib/Foundations/Semantics/LTS/Simulation.lean 6 7
Cslib/Foundations/Semantics/LTS/TraceEq.lean 4 6
Cslib/Foundations/Syntax/Congruence.lean 1 2
Cslib/Foundations/Syntax/Context.lean 3 0
Cslib/Foundations/Syntax/HasAlphaEquiv.lean 3 0
Cslib/Foundations/Syntax/HasSubstitution.lean 3 0
Cslib/Foundations/Syntax/HasWellFormed.lean 3 0
Cslib/Languages/CCS/Basic.lean 14 6
Cslib/Languages/CCS/BehaviouralTheory.lean 0 14
Cslib/Languages/CCS/Semantics.lean 5 0
Cslib/Languages/CombinatoryLogic/Basic.lean 43 28
Cslib/Languages/CombinatoryLogic/Confluence.lean 2 13
Cslib/Languages/CombinatoryLogic/Defs.lean 12 11
Cslib/Languages/CombinatoryLogic/Evaluation.lean 4 20
Cslib/Languages/CombinatoryLogic/Recursion.lean 27 30
Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean 7 3
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean 12 0
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean 22 43
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean 5 5
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean 0 2
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean 2 9
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean 2 13
Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean 2 19
Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean 3 7
Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean 1 4
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean 14 13
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean 3 8
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean 3 12
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean 2 6
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean 0 20
Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean 15 2
Cslib/Logics/HML/Basic.lean 9 15
Cslib/Logics/LinearLogic/CLL/Basic.lean 58 12
Cslib/Logics/LinearLogic/CLL/CutElimination.lean 2 0
Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean 2 2
Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean 45 111
CslibTests/LTS.lean 1 0