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

chore(library/init/lean/parser/macro): remove well_founded_tactics dependency

Browse source
This commit is contained in:
Leonardo de Moura 2018-04-30 11:11:23 -07:00
parent 0405a67a70
commit 3a494348b6
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/parser/macro.lean
View file

@ -6,7 +6,6 @@ Author: Sebastian Ullrich
prelude
import init.lean.parser.move
import init.lean.parser.syntax
import init.meta.well_founded_tactics
namespace lean.parser
@ -91,7 +90,6 @@ def flip_tag (tag : ℕ) : syntax → syntax
| (syntax.ident ident@{msc := some tag', ..}) :=
syntax.ident {ident with msc := if tag = tag' then none else some tag'}
| stx := stx
using_well_founded { dec_tac := tactic.admit } -- TODO
def expand : ℕ → syntax → exp_m syntax
| 0 _ := throw "macro expansion limit exceeded"
@ -116,7 +114,6 @@ do cfg ← read,
(arg_scopes.zip node.args).mmap' -- (uncurry resolve)
(λ ⟨sc, stx⟩, resolve sc stx)
| _ _ := pure ()
using_well_founded { dec_tac := tactic.admit }
def expand' (stx : syntax) : parse_m parse_state unit syntax :=
adapt_state (λ _, ({expand_state . next_tag := 0}, ())) (λ _, id) (expand 1000 stx)