-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathLambdaLab.lean
More file actions
116 lines (114 loc) · 4.85 KB
/
Copy pathLambdaLab.lean
File metadata and controls
116 lines (114 loc) · 4.85 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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
-- This module serves as the root of the `LambdaLab` library.
-- Import modules here that should be built as part of the library.
import LambdaLab.Relation.Closure
import LambdaLab.Relation.Normalization
import LambdaLab.Stlc.DeBruijn.Basic
import LambdaLab.Stlc.DeBruijn.Typing.Unification
import LambdaLab.Stlc.DeBruijn.TypeSystem
import LambdaLab.Stlc.DeBruijn.Typing.Basic
import LambdaLab.Stlc.DeBruijn.Step.Basic
import LambdaLab.Stlc.DeBruijn.Step.MStep
import LambdaLab.Stlc.DeBruijn.Step.Eval
import LambdaLab.Stlc.DeBruijn.Substitution
import LambdaLab.Stlc.DeBruijn.ParSubst
import LambdaLab.Stlc.DeBruijn.Typing.Reducibility
import LambdaLab.Stlc.DeBruijn.Typing.Properties
import LambdaLab.Stlc.DeBruijn.Typing.Preservation
import LambdaLab.Stlc.DeBruijn.Step.Confluence
import LambdaLab.Stlc.Named.Basic
import LambdaLab.Stlc.Named.Step.Basic
import LambdaLab.Stlc.Named.Step.MStep
import LambdaLab.Stlc.Named.Alpha
import LambdaLab.Stlc.Named.Typing.Basic
import LambdaLab.Stlc.Named.Typing.Principality
import LambdaLab.Stlc.Named.Typing.Properties
import LambdaLab.Stlc.Named.Translation
import LambdaLab.Stlc.Named.Step.Confluence
import LambdaLab.Stlc.Named.Typing.Preservation
import LambdaLab.Stlc.Named.Typing.Normalization
import LambdaLab.Stlc.Named.Step.Eval
import LambdaLab.Stlc.Named.Typing.Unification
import LambdaLab.Stlc.Named.Typing.W
import LambdaLab.Stlc.Named.Typing.J
import LambdaLab.Stlc.Named.Typing.D
import LambdaLab.Stlc.Named.Typing.S
import LambdaLab.Stlc.Named.Typing.Target
-- The parser stack, the categorical layer, the vernacular and the example languages.
--
-- These were previously outside the root, so `lake build` did not typecheck them and files
-- could (and did) rot undetected. Everything live is imported here now.
--
-- Deliberately excluded:
-- * Parser.IsoParser.Playground -- the prototype trail, kept as history. It is the only
-- unimported file in the tree; everything else here is built.
import LambdaLab.Parser.Numeral
import LambdaLab.Abstraction.Basic
import LambdaLab.Abstraction.Bicat
import LambdaLab.Abstraction.Chain
import LambdaLab.Abstraction.Freshen
import LambdaLab.Abstraction.Parens
import LambdaLab.Abstraction.Tokenizer
import LambdaLab.Arith.Pipeline
import LambdaLab.Inductive.Basic
import LambdaLab.Inductive.Example
import LambdaLab.Nominal.Atom
import LambdaLab.Nominal.Basic
import LambdaLab.Nominal.Instances
import LambdaLab.Nominal.Substitution
import LambdaLab.Nominal.Unification.Subst
import LambdaLab.Nominal.Unification.Signature
import LambdaLab.Nominal.Unification.Bridge
import LambdaLab.Nominal.Unification.Measure
import LambdaLab.Nominal.Unification.Basic
import LambdaLab.Nominal.Unification.Soundness
import LambdaLab.Nominal.Unification.Completeness
import LambdaLab.Nominal.Unification.MGU
import LambdaLab.TypeSystem.Named.Context
import LambdaLab.TypeSystem.Named.Basic
import LambdaLab.TypeSystem.Intrinsic.Basic
import LambdaLab.TypeSystem.DeBruijn.Context
import LambdaLab.TypeSystem.DeBruijn.Basic
import LambdaLab.TypeSystem.Bridge
import LambdaLab.TypeSystem.DeBruijn.Category
import LambdaLab.TypeSystem.Named.Category
import LambdaLab.TypeSystem.Bridged
import LambdaLab.Stlc.Named.Bridge
import LambdaLab.Stlc.Named.Bridged
import LambdaLab.TypeSystem.Named.Vernacular.Basic
import LambdaLab.TypeSystem.Named.Vernacular.Typing
import LambdaLab.TypeSystem.Named.Vernacular.Elaborate
import LambdaLab.TypeSystem.Named.Vernacular.Evaluate
import LambdaLab.Pipeline.Basic
-- NB: `FreeName` lives in `TypeSystem/` but sits *above* `Pipeline.Basic`, since the atoms
-- it constructs are carved out of the grammar's reserved `Token`s. It is the one place the two
-- folders' layering is inverted.
import LambdaLab.TypeSystem.Named.FreeName
import LambdaLab.Pipeline.Stages.Parse
import LambdaLab.Pipeline.Stages.Elaborate
import LambdaLab.Pipeline.Stages.Evaluate
import LambdaLab.Pipeline.Compose
import LambdaLab.Pipeline.Cli
import LambdaLab.Pipeline.Example
import LambdaLab.NEList
import LambdaLab.Parser.IsoParser.Adapters
import LambdaLab.Parser.IsoParser.Basic
import LambdaLab.Parser.IsoParser.Combinators
import LambdaLab.Parser.IsoParser.Example
import LambdaLab.Parser.IsoParser.Fix
import LambdaLab.Parser.IsoParser.Mixfix.Basic
import LambdaLab.Parser.IsoParser.Mixfix.Biparser
import LambdaLab.Parser.IsoParser.Mixfix.Complete
import LambdaLab.Parser.IsoParser.Mixfix.Exact
import LambdaLab.Parser.IsoParser.Mixfix.Parse
import LambdaLab.Parser.IsoParser.Mixfix.Sound
import LambdaLab.Parser.IsoParser.Mixfix.Tree
import LambdaLab.Parser.IsoParser.Mixfix.Unambiguity
import LambdaLab.Parser.IsoParser.Notation
import LambdaLab.Parser.IsoParser.Token
import LambdaLab.Parser.IsoParser.Tokenize
import LambdaLab.Parser.LossyParser.Basic
import LambdaLab.Parser.Truncation
import LambdaLab.Parser.Truncation.Mixfix
import LambdaLab.Stlc.Named.Pipeline
import LambdaLab.Stlc.Named.TypeSystem
import LambdaLab.Stlc.Named.Typing.JComplete