forked from leanprover/cslib
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathCslib.lean
More file actions
100 lines (99 loc) · 5.46 KB
/
Cslib.lean
File metadata and controls
100 lines (99 loc) · 5.46 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
module -- shake: keep-all
public import Cslib.Algorithms.Lean.MergeSort.MergeSort
public import Cslib.Algorithms.Lean.TimeM
public import Cslib.Computability.Automata.Acceptors.Acceptor
public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
public import Cslib.Computability.Automata.DA.Basic
public import Cslib.Computability.Automata.DA.Buchi
public import Cslib.Computability.Automata.DA.Congr
public import Cslib.Computability.Automata.DA.Prod
public import Cslib.Computability.Automata.DA.ToNA
public import Cslib.Computability.Automata.EpsilonNA.Basic
public import Cslib.Computability.Automata.EpsilonNA.ToNA
public import Cslib.Computability.Automata.NA.Basic
public import Cslib.Computability.Automata.NA.BuchiEquiv
public import Cslib.Computability.Automata.NA.BuchiInter
public import Cslib.Computability.Automata.NA.Concat
public import Cslib.Computability.Automata.NA.Hist
public import Cslib.Computability.Automata.NA.Loop
public import Cslib.Computability.Automata.NA.Pair
public import Cslib.Computability.Automata.NA.Prod
public import Cslib.Computability.Automata.NA.Sum
public import Cslib.Computability.Automata.NA.ToDA
public import Cslib.Computability.Automata.NA.Total
public import Cslib.Computability.Languages.Congruences.BuchiCongruence
public import Cslib.Computability.Languages.Congruences.RightCongruence
public import Cslib.Computability.Languages.ExampleEventuallyZero
public import Cslib.Computability.Languages.Language
public import Cslib.Computability.Languages.OmegaLanguage
public import Cslib.Computability.Languages.OmegaRegularLanguage
public import Cslib.Computability.Languages.RegularLanguage
public import Cslib.Computability.Machines.SingleTapeTuring.Basic
public import Cslib.Computability.URM.Basic
public import Cslib.Computability.URM.Computable
public import Cslib.Computability.URM.Defs
public import Cslib.Computability.URM.Execution
public import Cslib.Computability.URM.StandardForm
public import Cslib.Computability.URM.StraightLine
public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
public import Cslib.Foundations.Control.Monad.Free
public import Cslib.Foundations.Control.Monad.Free.Effects
public import Cslib.Foundations.Control.Monad.Free.Fold
public import Cslib.Foundations.Data.BiTape
public import Cslib.Foundations.Data.FinFun
public import Cslib.Foundations.Data.HasFresh
public import Cslib.Foundations.Data.Nat.Segment
public import Cslib.Foundations.Data.OmegaSequence.Defs
public import Cslib.Foundations.Data.OmegaSequence.Flatten
public import Cslib.Foundations.Data.OmegaSequence.InfOcc
public import Cslib.Foundations.Data.OmegaSequence.Init
public import Cslib.Foundations.Data.OmegaSequence.Temporal
public import Cslib.Foundations.Data.RelatesInSteps
public import Cslib.Foundations.Data.Relation
public import Cslib.Foundations.Data.Set.Saturation
public import Cslib.Foundations.Data.StackTape
public import Cslib.Foundations.Lint.Basic
public import Cslib.Foundations.Semantics.FLTS.Basic
public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
public import Cslib.Foundations.Semantics.FLTS.Prod
public import Cslib.Foundations.Semantics.LTS.Basic
public import Cslib.Foundations.Semantics.LTS.Bisimulation
public import Cslib.Foundations.Semantics.LTS.Simulation
public import Cslib.Foundations.Semantics.LTS.TraceEq
public import Cslib.Foundations.Syntax.Congruence
public import Cslib.Foundations.Syntax.Context
public import Cslib.Foundations.Syntax.HasAlphaEquiv
public import Cslib.Foundations.Syntax.HasSubstitution
public import Cslib.Foundations.Syntax.HasWellFormed
public import Cslib.Init
public import Cslib.Languages.CCS.Basic
public import Cslib.Languages.CCS.BehaviouralTheory
public import Cslib.Languages.CCS.Semantics
public import Cslib.Languages.CombinatoryLogic.Basic
public import Cslib.Languages.CombinatoryLogic.Confluence
public import Cslib.Languages.CombinatoryLogic.Defs
public import Cslib.Languages.CombinatoryLogic.Evaluation
public import Cslib.Languages.CombinatoryLogic.List
public import Cslib.Languages.CombinatoryLogic.Recursion
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
public import Cslib.Logics.HML.Basic
public import Cslib.Logics.LinearLogic.CLL.Basic
public import Cslib.Logics.LinearLogic.CLL.CutElimination
public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic