-
Notifications
You must be signed in to change notification settings - Fork 327
/
Elab.lean
43 lines (43 loc) · 1.21 KB
/
Elab.lean
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
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Import
import Lean.Elab.Exception
import Lean.Elab.Config
import Lean.Elab.Command
import Lean.Elab.Term
import Lean.Elab.App
import Lean.Elab.Binders
import Lean.Elab.LetRec
import Lean.Elab.Frontend
import Lean.Elab.BuiltinNotation
import Lean.Elab.Declaration
import Lean.Elab.Tactic
import Lean.Elab.Match
-- HACK: must come after `Match` because builtin elaborators (for `match` in this case) do not take priorities
import Lean.Elab.Quotation
import Lean.Elab.Syntax
import Lean.Elab.Do
import Lean.Elab.StructInst
import Lean.Elab.Inductive
import Lean.Elab.Structure
import Lean.Elab.Print
import Lean.Elab.MutualDef
import Lean.Elab.AuxDef
import Lean.Elab.PreDefinition
import Lean.Elab.Deriving
import Lean.Elab.DeclarationRange
import Lean.Elab.Extra
import Lean.Elab.GenInjective
import Lean.Elab.BuiltinTerm
import Lean.Elab.Arg
import Lean.Elab.PatternVar
import Lean.Elab.ElabRules
import Lean.Elab.Macro
import Lean.Elab.Notation
import Lean.Elab.Mixfix
import Lean.Elab.MacroRules
import Lean.Elab.BuiltinCommand
import Lean.Elab.RecAppSyntax