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

perf: handle easy case efficiently

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-22 18:55:13 -07:00
parent 661548a2fe
commit 3586337c56
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/KAbstract.lean
View file

@ -35,7 +35,10 @@ private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : Hea
visitChildren ()
def kabstract {m} [MonadLiftT MetaM m] (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : m Expr := liftMetaM do
(kabstractAux occs p p.toHeadIndex p.headNumArgs e 0).run' 1
if p.isFVar && occs == Occurrences.all then
pure $ e.abstract #[p] -- Easy case
else
(kabstractAux occs p p.toHeadIndex p.headNumArgs e 0).run' 1
end Meta
end Lean