From bc4b3047a9beee2aaf4096f6f9c2e33bee568d51 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 20 Feb 2020 13:09:22 -0800 Subject: [PATCH] feat: add `whnfHeadPred` and `whnfUntil` --- src/Init/Lean/Meta/WHNF.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/Init/Lean/Meta/WHNF.lean b/src/Init/Lean/Meta/WHNF.lean index e383e5cac7..84ce45baec 100644 --- a/src/Init/Lean/Meta/WHNF.lean +++ b/src/Init/Lean/Meta/WHNF.lean @@ -49,5 +49,22 @@ match e.getAppFn with | _ => pure none | _ => pure none +@[specialize] private partial def whnfHeadPredAux (pred : Expr → MetaM Bool) : Expr → MetaM Expr +| e => Lean.WHNF.whnfEasyCases getLocalDecl getExprMVarAssignment? e $ fun e => do + e ← whnfCore e; + condM (pred e) + (do + e? ← unfoldDefinition? e; + match e? with + | some e => whnfHeadPredAux e + | none => pure e) + (pure e) + +def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr := +whnfHeadPredAux pred e + +def whnfUntil (e : Expr) (declName : Name) : MetaM Expr := +whnfHeadPredAux (fun e => pure $ e.isAppOf declName) e + end Meta end Lean