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

fix: isHeadBetaTarget

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-05 10:24:38 -08:00
parent 74c9d54362
commit 2f60e82049
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Lean/Expr.lean
View file

@ -694,14 +694,17 @@ def betaRev (f : Expr) (revArgs : Array Expr) : Expr :=
if revArgs.size == 0 then f
else betaRevAux revArgs revArgs.size f 0
def isHeadBetaTarget : Expr → Bool
def isHeadBetaTargetFn : Expr → Bool
| Expr.lam _ _ _ _ => true
| Expr.mdata _ b _ => isHeadBetaTarget b
| Expr.mdata _ b _ => isHeadBetaTargetFn b
| _ => false
def headBeta (e : Expr) : Expr :=
let f := e.getAppFn;
if f.isHeadBetaTarget then betaRev f e.getAppRevArgs else e
if f.isHeadBetaTargetFn then betaRev f e.getAppRevArgs else e
def isHeadBetaTarget (e : Expr) : Bool :=
e.getAppFn.isHeadBetaTargetFn
private def etaExpandedBody : Expr → Nat → Nat → Option Expr
| app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none