|
Cslib/Algorithms/Lean/MergeSort/MergeSort.lean |
6 |
16 |
|
|
Cslib/Algorithms/Lean/TimeM.lean |
16 |
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 |
1 |
3 |
|
|
Cslib/Computability/Languages/Congruences/BuchiCongruence.lean |
3 |
6 |
|
|
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 |
16 |
|
|
Cslib/Computability/Languages/RegularLanguage.lean |
0 |
13 |
|
|
Cslib/Computability/Machines/SingleTapeTuring/Basic.lean |
36 |
7 |
|
|
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/Combinatorics/InfiniteGraphRamsey.lean |
0 |
2 |
|
|
Cslib/Foundations/Control/Monad/Free.lean |
10 |
27 |
|
|
Cslib/Foundations/Control/Monad/Free/Effects.lean |
33 |
31 |
|
|
Cslib/Foundations/Control/Monad/Free/Fold.lean |
1 |
3 |
|
|
Cslib/Foundations/Data/BiTape.lean |
15 |
6 |
|
|
Cslib/Foundations/Data/FinFun.lean |
8 |
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 |
4 |
|
|
Cslib/Foundations/Data/OmegaSequence/Init.lean |
1 |
109 |
|
|
Cslib/Foundations/Data/OmegaSequence/Temporal.lean |
2 |
9 |
|
|
Cslib/Foundations/Data/RelatesInSteps.lean |
2 |
23 |
|
|
Cslib/Foundations/Data/Relation.lean |
23 |
51 |
|
|
Cslib/Foundations/Data/Set/Saturation.lean |
1 |
2 |
|
|
Cslib/Foundations/Data/StackTape.lean |
10 |
15 |
|
|
Cslib/Foundations/Lint/Basic.lean |
1 |
0 |
|
|
Cslib/Foundations/Logic/InferenceSystem.lean |
8 |
1 |
|
|
Cslib/Foundations/Logic/LogicalEquivalence.lean |
4 |
1 |
|
|
Cslib/Foundations/Semantics/FLTS/Basic.lean |
3 |
2 |
|
|
Cslib/Foundations/Semantics/FLTS/FLTSToLTS.lean |
2 |
4 |
|
|
Cslib/Foundations/Semantics/FLTS/LTSToFLTS.lean |
1 |
3 |
|
|
Cslib/Foundations/Semantics/FLTS/Prod.lean |
1 |
1 |
|
|
Cslib/Foundations/Semantics/LTS/Basic.lean |
15 |
26 |
|
|
Cslib/Foundations/Semantics/LTS/Bisimulation.lean |
21 |
39 |
|
|
Cslib/Foundations/Semantics/LTS/Divergence.lean |
3 |
2 |
|
|
Cslib/Foundations/Semantics/LTS/Execution.lean |
1 |
10 |
|
|
Cslib/Foundations/Semantics/LTS/HasTau.lean |
6 |
8 |
|
|
Cslib/Foundations/Semantics/LTS/Notation.lean |
3 |
0 |
|
|
Cslib/Foundations/Semantics/LTS/OmegaExecution.lean |
1 |
6 |
|
|
Cslib/Foundations/Semantics/LTS/Relation.lean |
7 |
0 |
|
|
Cslib/Foundations/Semantics/LTS/Simulation.lean |
11 |
7 |
|
|
Cslib/Foundations/Semantics/LTS/Termination.lean |
2 |
0 |
|
|
Cslib/Foundations/Semantics/LTS/Total.lean |
4 |
8 |
|
|
Cslib/Foundations/Semantics/LTS/TraceEq.lean |
6 |
6 |
|
|
Cslib/Foundations/Semantics/LTS/Union.lean |
5 |
0 |
|
|
Cslib/Foundations/Syntax/Congruence.lean |
0 |
2 |
|
|
Cslib/Foundations/Syntax/Context.lean |
4 |
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 |
6 |
0 |
|
|
Cslib/Languages/CombinatoryLogic/Basic.lean |
43 |
30 |
|
|
Cslib/Languages/CombinatoryLogic/Confluence.lean |
3 |
13 |
|
|
Cslib/Languages/CombinatoryLogic/Defs.lean |
11 |
11 |
|
|
Cslib/Languages/CombinatoryLogic/Evaluation.lean |
4 |
20 |
|
|
Cslib/Languages/CombinatoryLogic/List.lean |
17 |
25 |
|
|
Cslib/Languages/CombinatoryLogic/Recursion.lean |
38 |
44 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean |
12 |
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/Stlc/StrongNorm.lean |
4 |
9 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean |
14 |
13 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Congruence.lean |
2 |
1 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean |
4 |
19 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean |
3 |
12 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean |
3 |
2 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean |
4 |
16 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean |
0 |
1 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean |
2 |
8 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiApp.lean |
4 |
9 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean |
4 |
6 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean |
0 |
23 |
|
|
Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean |
2 |
11 |
|
|
Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean |
15 |
2 |
|
|
Cslib/Logics/HML/Basic.lean |
9 |
15 |
|
|
Cslib/Logics/HML/LogicalEquivalence.lean |
13 |
4 |
|
|
Cslib/Logics/LinearLogic/CLL/Basic.lean |
64 |
14 |
|
|
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 |
|