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
This commit is contained in:
Leonardo de Moura 2020-10-16 11:55:10 -07:00
parent eabee9ce7e
commit 65abb119f5
3 changed files with 449 additions and 458 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -11,11 +11,13 @@ import Lean.Elab.SyntheticMVars
import Lean.Elab.DeclModifiers
namespace Lean
namespace MonadResolveName end MonadResolveName -- Hack for old frontend
open MonadResolveName (getCurrNamespace getOpenDecls) -- HACK for old frontend
namespace Elab
namespace Term end Term -- Hack for old frontend
open Term (TermElabM) -- Hack for old fronted
namespace Command
structure Scope :=

897
src/Lean/Elab/Term.lean
View file

File diff suppressed because it is too large Load diff

6
tests/lean/sanitizeMacroScopes.lean.expected.out
View file

@ -1,9 +1,9 @@
[Elab.step] #check fun x => m x
fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m
[Elab.step] none fun x => m x
[Elab.step] Sort _ _
[Elab.step] some Sort.{?_uniq.328} _
[Elab.step] none m x
[Elab.step] none fun x✝ => x
[Elab.step] Sort _ _
[Elab.step] some Sort.{?_uniq.331} _
[Elab.step] none x
fun (x : ?m) (x_1 : ?m x) => x : (x : ?m) → ?m x → ?m
[Elab.step] end