Skip to content

Commit fb557ae

Browse files
tannerduvetannerduve
committed
mk all
1 parent 2574110 commit fb557ae

2 files changed

Lines changed: 118 additions & 120 deletions

File tree

‎Cslib.lean‎

Lines changed: 106 additions & 106 deletions
Original file line numberDiff line numberDiff line change
@@ -1,106 +1,106 @@
1-
module -- shake: keep-all
2-
3-
public import Cslib.Algorithms.Lean.MergeSort.MergeSort
4-
public import Cslib.Algorithms.Lean.TimeM
5-
public import Cslib.Computability.Automata.Acceptors.Acceptor
6-
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
7-
public import Cslib.Computability.Automata.DA.Basic
8-
public import Cslib.Computability.Automata.DA.Buchi
9-
public import Cslib.Computability.Automata.DA.Congr
10-
public import Cslib.Computability.Automata.DA.Prod
11-
public import Cslib.Computability.Automata.DA.ToNA
12-
public import Cslib.Computability.Automata.EpsilonNA.Basic
13-
public import Cslib.Computability.Automata.EpsilonNA.ToNA
14-
public import Cslib.Computability.Automata.NA.Basic
15-
public import Cslib.Computability.Automata.NA.BuchiEquiv
16-
public import Cslib.Computability.Automata.NA.BuchiInter
17-
public import Cslib.Computability.Automata.NA.Concat
18-
public import Cslib.Computability.Automata.NA.Hist
19-
public import Cslib.Computability.Automata.NA.Loop
20-
public import Cslib.Computability.Automata.NA.Pair
21-
public import Cslib.Computability.Automata.NA.Prod
22-
public import Cslib.Computability.Automata.NA.Sum
23-
public import Cslib.Computability.Automata.NA.ToDA
24-
public import Cslib.Computability.Automata.NA.Total
25-
public import Cslib.Computability.Languages.Congruences.BuchiCongruence
26-
public import Cslib.Computability.Languages.Congruences.RightCongruence
27-
public import Cslib.Computability.Languages.ExampleEventuallyZero
28-
public import Cslib.Computability.Languages.Language
29-
public import Cslib.Computability.Languages.OmegaLanguage
30-
public import Cslib.Computability.Languages.OmegaRegularLanguage
31-
public import Cslib.Computability.Languages.RegularLanguage
32-
public import Cslib.Computability.Machines.SingleTapeTuring.Basic
33-
public import Cslib.Computability.URM.Basic
34-
public import Cslib.Computability.URM.Computable
35-
public import Cslib.Computability.URM.Defs
36-
public import Cslib.Computability.URM.Execution
37-
public import Cslib.Computability.URM.StandardForm
38-
public import Cslib.Computability.URM.StraightLine
39-
public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
40-
public import Cslib.Foundations.Control.Monad.Free
41-
public import Cslib.Foundations.Control.Monad.Free.Effects
42-
public import Cslib.Foundations.Control.Monad.Free.Fold
43-
public import Cslib.Foundations.Data.BiTape
44-
public import Cslib.Foundations.Data.FinFun
45-
public import Cslib.Foundations.Data.HasFresh
46-
public import Cslib.Foundations.Data.Nat.Segment
47-
public import Cslib.Foundations.Data.OmegaSequence.Defs
48-
public import Cslib.Foundations.Data.OmegaSequence.Flatten
49-
public import Cslib.Foundations.Data.OmegaSequence.InfOcc
50-
public import Cslib.Foundations.Data.OmegaSequence.Init
51-
public import Cslib.Foundations.Data.OmegaSequence.Temporal
52-
public import Cslib.Foundations.Data.RelatesInSteps
53-
public import Cslib.Foundations.Data.Relation
54-
public import Cslib.Foundations.Data.Set.Saturation
55-
public import Cslib.Foundations.Data.StackTape
56-
public import Cslib.Foundations.Lint.Basic
57-
public import Cslib.Foundations.Logic.InferenceSystem
58-
public import Cslib.Foundations.Logic.LogicalEquivalence
59-
public import Cslib.Foundations.Semantics.FLTS.Basic
60-
public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
61-
public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
62-
public import Cslib.Foundations.Semantics.FLTS.Prod
63-
public import Cslib.Foundations.Semantics.LTS.Basic
64-
public import Cslib.Foundations.Semantics.LTS.Bisimulation
65-
public import Cslib.Foundations.Semantics.LTS.Simulation
66-
public import Cslib.Foundations.Semantics.LTS.TraceEq
67-
public import Cslib.Foundations.Syntax.Congruence
68-
public import Cslib.Foundations.Syntax.Context
69-
public import Cslib.Foundations.Syntax.HasAlphaEquiv
70-
public import Cslib.Foundations.Syntax.HasSubstitution
71-
public import Cslib.Foundations.Syntax.HasWellFormed
72-
public import Cslib.Init
73-
public import Cslib.Languages.CCS.Basic
74-
public import Cslib.Languages.CCS.BehaviouralTheory
75-
public import Cslib.Languages.CCS.Semantics
76-
public import Cslib.Languages.CombinatoryLogic.Basic
77-
public import Cslib.Languages.CombinatoryLogic.Confluence
78-
public import Cslib.Languages.CombinatoryLogic.Defs
79-
public import Cslib.Languages.CombinatoryLogic.Evaluation
80-
public import Cslib.Languages.CombinatoryLogic.List
81-
public import Cslib.Languages.CombinatoryLogic.Recursion
82-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
83-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
84-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
85-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
86-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
87-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
88-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
89-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
90-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
91-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
92-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
93-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
94-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
95-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
96-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
97-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
98-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
99-
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
100-
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
101-
public import Cslib.Logics.HML.Basic
102-
public import Cslib.Logics.HML.LogicalEquivalence
103-
public import Cslib.Logics.LinearLogic.CLL.Basic
104-
public import Cslib.Logics.LinearLogic.CLL.CutElimination
105-
public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
106-
public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
1+
import Cslib.Algorithms.Lean.MergeSort.MergeSort
2+
import Cslib.Algorithms.Lean.TimeM
3+
import Cslib.Computability.Automata.Acceptors.Acceptor
4+
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
5+
import Cslib.Computability.Automata.DA.Basic
6+
import Cslib.Computability.Automata.DA.Buchi
7+
import Cslib.Computability.Automata.DA.Congr
8+
import Cslib.Computability.Automata.DA.Prod
9+
import Cslib.Computability.Automata.DA.ToNA
10+
import Cslib.Computability.Automata.EpsilonNA.Basic
11+
import Cslib.Computability.Automata.EpsilonNA.ToNA
12+
import Cslib.Computability.Automata.NA.Basic
13+
import Cslib.Computability.Automata.NA.BuchiEquiv
14+
import Cslib.Computability.Automata.NA.BuchiInter
15+
import Cslib.Computability.Automata.NA.Concat
16+
import Cslib.Computability.Automata.NA.Hist
17+
import Cslib.Computability.Automata.NA.Loop
18+
import Cslib.Computability.Automata.NA.Pair
19+
import Cslib.Computability.Automata.NA.Prod
20+
import Cslib.Computability.Automata.NA.Sum
21+
import Cslib.Computability.Automata.NA.ToDA
22+
import Cslib.Computability.Automata.NA.Total
23+
import Cslib.Computability.Languages.Congruences.BuchiCongruence
24+
import Cslib.Computability.Languages.Congruences.RightCongruence
25+
import Cslib.Computability.Languages.ExampleEventuallyZero
26+
import Cslib.Computability.Languages.Language
27+
import Cslib.Computability.Languages.OmegaLanguage
28+
import Cslib.Computability.Languages.OmegaRegularLanguage
29+
import Cslib.Computability.Languages.RegularLanguage
30+
import Cslib.Computability.Machines.SingleTapeTuring.Basic
31+
import Cslib.Computability.URM.Basic
32+
import Cslib.Computability.URM.Computable
33+
import Cslib.Computability.URM.Defs
34+
import Cslib.Computability.URM.Execution
35+
import Cslib.Computability.URM.StandardForm
36+
import Cslib.Computability.URM.StraightLine
37+
import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
38+
import Cslib.Foundations.Control.Monad.Free
39+
import Cslib.Foundations.Control.Monad.Free.Effects
40+
import Cslib.Foundations.Control.Monad.Free.Fold
41+
import Cslib.Foundations.Data.BiTape
42+
import Cslib.Foundations.Data.FinFun
43+
import Cslib.Foundations.Data.HasFresh
44+
import Cslib.Foundations.Data.Nat.Segment
45+
import Cslib.Foundations.Data.OmegaSequence.Defs
46+
import Cslib.Foundations.Data.OmegaSequence.Flatten
47+
import Cslib.Foundations.Data.OmegaSequence.InfOcc
48+
import Cslib.Foundations.Data.OmegaSequence.Init
49+
import Cslib.Foundations.Data.OmegaSequence.Temporal
50+
import Cslib.Foundations.Data.RelatesInSteps
51+
import Cslib.Foundations.Data.Relation
52+
import Cslib.Foundations.Data.Set.Saturation
53+
import Cslib.Foundations.Data.StackTape
54+
import Cslib.Foundations.Lint.Basic
55+
import Cslib.Foundations.Logic.InferenceSystem
56+
import Cslib.Foundations.Logic.LogicalEquivalence
57+
import Cslib.Foundations.Semantics.FLTS.Basic
58+
import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
59+
import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
60+
import Cslib.Foundations.Semantics.FLTS.Prod
61+
import Cslib.Foundations.Semantics.LTS.Basic
62+
import Cslib.Foundations.Semantics.LTS.Bisimulation
63+
import Cslib.Foundations.Semantics.LTS.Simulation
64+
import Cslib.Foundations.Semantics.LTS.TraceEq
65+
import Cslib.Foundations.Syntax.Congruence
66+
import Cslib.Foundations.Syntax.Context
67+
import Cslib.Foundations.Syntax.HasAlphaEquiv
68+
import Cslib.Foundations.Syntax.HasSubstitution
69+
import Cslib.Foundations.Syntax.HasWellFormed
70+
import Cslib.Init
71+
import Cslib.Languages.CCS.Basic
72+
import Cslib.Languages.CCS.BehaviouralTheory
73+
import Cslib.Languages.CCS.Semantics
74+
import Cslib.Languages.CombinatoryLogic.Basic
75+
import Cslib.Languages.CombinatoryLogic.Confluence
76+
import Cslib.Languages.CombinatoryLogic.Defs
77+
import Cslib.Languages.CombinatoryLogic.Evaluation
78+
import Cslib.Languages.CombinatoryLogic.List
79+
import Cslib.Languages.CombinatoryLogic.Recursion
80+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
81+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
82+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
83+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
84+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
85+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
86+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
87+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
88+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
89+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
90+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
91+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
92+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
93+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
94+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
95+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
96+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
97+
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
98+
import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
99+
import Cslib.Logics.HML.Basic
100+
import Cslib.Logics.HML.LogicalEquivalence
101+
import Cslib.Logics.LinearLogic.CLL.Basic
102+
import Cslib.Logics.LinearLogic.CLL.CutElimination
103+
import Cslib.Logics.LinearLogic.CLL.EtaExpansion
104+
import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
105+
import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Completeness
106+
import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Soundness

‎CslibTests.lean‎

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,12 @@
1-
module -- shake: keep-all
2-
3-
public import CslibTests.Bisimulation
4-
public import CslibTests.CCS
5-
public import CslibTests.CLL
6-
public import CslibTests.DFA
7-
public import CslibTests.FreeMonad
8-
public import CslibTests.GrindLint
9-
public import CslibTests.HML
10-
public import CslibTests.HasFresh
11-
public import CslibTests.ImportWithMathlib
12-
public import CslibTests.LTS
13-
public import CslibTests.LambdaCalculus
14-
public import CslibTests.Reduction
1+
import CslibTests.Bisimulation
2+
import CslibTests.CCS
3+
import CslibTests.CLL
4+
import CslibTests.DFA
5+
import CslibTests.FreeMonad
6+
import CslibTests.GrindLint
7+
import CslibTests.HML
8+
import CslibTests.HasFresh
9+
import CslibTests.ImportWithMathlib
10+
import CslibTests.LTS
11+
import CslibTests.LambdaCalculus
12+
import CslibTests.Reduction

0 commit comments

Comments
 (0)