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

chore: move to new frontend

Browse source 
@Kha another significant milestone: all files at `src/Lean/Meta` are
being compiled with the new frontend.
This commit is contained in:
Leonardo de Moura 2020-10-20 10:55:07 -07:00
parent 0f126dd566
commit 80a0200ab2
4 changed files with 323 additions and 335 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Delaborator.lean
View file

@ -31,6 +31,8 @@ import Lean.Syntax
import Lean.Elab.Term
namespace Lean
namespace Meta end Meta -- HACK for old frontend
open Meta (MetaM) -- HACK for old frontend
-- TODO: move, maybe
namespace Level

651
src/Lean/Meta/Basic.lean
View file

File diff suppressed because it is too large Load diff

3
src/Lean/ParserCompiler.lean
View file

@ -15,6 +15,9 @@ import Lean.ParserCompiler.Attribute
import Lean.Parser.Extension
namespace Lean
namespace Meta end Meta -- HACK for old frontend
open Meta (MetaM) -- HACK for old frontend
namespace ParserCompiler
structure Context (α : Type) :=

2
src/Lean/PrettyPrinter.lean
View file

@ -9,6 +9,8 @@ import Lean.PrettyPrinter.Formatter
import Lean.Parser.Module
namespace Lean
namespace Meta end Meta -- HACK for old frontend
open Meta (MetaM) -- HACK for old frontend
def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }