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
57 lines (57 loc) · 2.84 KB
/
Copy pathCslib.lean
File metadata and controls
57 lines (57 loc) · 2.84 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
import Cslib.Computability.Automata.DA
import Cslib.Computability.Automata.DFA
import Cslib.Computability.Automata.DFAToNFA
import Cslib.Computability.Automata.EpsilonNFA
import Cslib.Computability.Automata.EpsilonNFAToNFA
import Cslib.Computability.Automata.NA
import Cslib.Computability.Automata.NFA
import Cslib.Computability.Automata.NFAToDFA
import Cslib.Computability.Languages.Language
import Cslib.Computability.Languages.OmegaLanguage
import Cslib.Foundations.Control.Monad.Free
import Cslib.Foundations.Control.Monad.Free.Effects
import Cslib.Foundations.Control.Monad.Free.Fold
import Cslib.Foundations.Data.FinFun
import Cslib.Foundations.Data.HasFresh
import Cslib.Foundations.Data.Nat.Segment
import Cslib.Foundations.Data.OmegaSequence.Defs
import Cslib.Foundations.Data.OmegaSequence.Flatten
import Cslib.Foundations.Data.OmegaSequence.Init
import Cslib.Foundations.Data.Relation
import Cslib.Foundations.Lint.Basic
import Cslib.Foundations.Semantics.LTS.Basic
import Cslib.Foundations.Semantics.LTS.Bisimulation
import Cslib.Foundations.Semantics.LTS.Simulation
import Cslib.Foundations.Semantics.LTS.TraceEq
import Cslib.Foundations.Semantics.ReductionSystem.Basic
import Cslib.Foundations.Syntax.HasAlphaEquiv
import Cslib.Foundations.Syntax.HasSubstitution
import Cslib.Foundations.Syntax.HasWellFormed
import Cslib.Init
import Cslib.Languages.CCS.Basic
import Cslib.Languages.CCS.BehaviouralTheory
import Cslib.Languages.CCS.Semantics
import Cslib.Languages.CombinatoryLogic.Basic
import Cslib.Languages.CombinatoryLogic.Confluence
import Cslib.Languages.CombinatoryLogic.Defs
import Cslib.Languages.CombinatoryLogic.Evaluation
import Cslib.Languages.CombinatoryLogic.Recursion
import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
import Cslib.Logics.LinearLogic.CLL.Basic
import Cslib.Logics.LinearLogic.CLL.CutElimination
import Cslib.Logics.LinearLogic.CLL.MProof
import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic