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

chore: cleanup betaRev (#4921)

Browse source
This commit is contained in:
Leonardo de Moura 2024-08-05 20:02:20 +02:00 • committed by GitHub
parent d671d0d61a
commit 590de785cc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Lean/Expr.lean
View file

@ -1452,28 +1452,26 @@ partial def betaRev (f : Expr) (revArgs : Array Expr) (useZeta := false) (preser
else
let sz := revArgs.size
let rec go (e : Expr) (i : Nat) : Expr :=
let done (_ : Unit) : Expr :=
let n := sz - i
mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
match e with
| Expr.lam _ _ b _ =>
| .lam _ _ b _ =>
if i + 1 < sz then
go b (i+1)
else
let n := sz - (i + 1)
mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs
| Expr.letE _ _ v b _ =>
b.instantiate revArgs
| .letE _ _ v b _ =>
if useZeta && i < sz then
go (b.instantiate1 v) i
else
let n := sz - i
mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
| Expr.mdata k b =>
done ()
| .mdata _ b =>
if preserveMData then
let n := sz - i
mkMData k (mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs)
done ()
else
go b i
| b =>
let n := sz - i
mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs
| _ => done ()
go f 0
/--