max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: file name convention

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-08 11:21:38 -08:00
parent 29f0a1c4c9
commit 79f30d5c8c
10 changed files with 10 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Lean/Elab.lean
View file

@ -6,11 +6,11 @@ Authors: Leonardo de Moura
prelude
import Init.Lean.Elab.Import
import Init.Lean.Elab.Exception
import Init.Lean.Elab.ElabStrategyAttrs
import Init.Lean.Elab.StrategyAttrs
import Init.Lean.Elab.Command
import Init.Lean.Elab.Term
import Init.Lean.Elab.TermApp
import Init.Lean.Elab.TermBinders
import Init.Lean.Elab.App
import Init.Lean.Elab.Binders
import Init.Lean.Elab.Quotation
import Init.Lean.Elab.Frontend
import Init.Lean.Elab.BuiltinNotation

0
src/Init/Lean/Elab/TermApp.lean → src/Init/Lean/Elab/App.lean
View file

0
src/Init/Lean/Elab/TermBinders.lean → src/Init/Lean/Elab/Binders.lean
View file

4
src/Init/Lean/Elab/Command.lean
View file

@ -8,8 +8,8 @@ import Init.Lean.Elab.Alias
import Init.Lean.Elab.Log
import Init.Lean.Elab.ResolveName
import Init.Lean.Elab.Term
import Init.Lean.Elab.TermBinders
import Init.Lean.Elab.SynthesizeSyntheticMVars
import Init.Lean.Elab.Binders
import Init.Lean.Elab.SyntheticMVars
namespace Lean
namespace Elab

2
src/Init/Lean/Elab/Definition.lean
View file

@ -7,7 +7,7 @@ prelude
import Init.Lean.Util.CollectLevelParams
import Init.Lean.Util.CollectFVars
import Init.Lean.Elab.DeclModifiers
import Init.Lean.Elab.TermBinders
import Init.Lean.Elab.Binders
namespace Lean
namespace Elab

2
src/Init/Lean/Elab/DoNotation.lean
View file

@ -5,7 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Elab.Term
import Init.Lean.Elab.TermBinders
import Init.Lean.Elab.Binders
import Init.Lean.Elab.Quotation
namespace Lean

0
src/Init/Lean/Elab/ElabStrategyAttrs.lean → src/Init/Lean/Elab/StrategyAttrs.lean
View file

5
src/Init/Lean/Elab/StructInst.lean
View file

@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Elab.Term
import Init.Lean.Elab.TermApp
import Init.Lean.Elab.TermBinders
import Init.Lean.Elab.App
import Init.Lean.Elab.Binders
import Init.Lean.Elab.Quotation
namespace Lean

0
src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean → src/Init/Lean/Elab/SyntheticMVars.lean
View file

2
src/Init/Lean/Elab/Tactic/ElabTerm.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Lean.Meta.Tactic.Apply
import Init.Lean.Elab.Tactic.Basic
import Init.Lean.Elab.SynthesizeSyntheticMVars
import Init.Lean.Elab.SyntheticMVars
namespace Lean
namespace Elab