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

fix: make getArg!' compute the correct arg index to access (#10567)

Browse source 
This PR fixes argument index calculation in `Lean.Expr.getArg!'`.
This commit is contained in:
Sebastian Graf 2025-09-26 13:54:49 +02:00 • committed by GitHub
parent 71e09ca883
commit 62fd973b28
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Expr.lean
View file

@ -1267,7 +1267,7 @@ def getRevArg!' : Expr → Nat → Expr
getRevArg! e (n - i - 1)
/-- Similar to `getArg!`, but skips mdata -/
@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs') : Expr :=
getRevArg!' e (n - i - 1)
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/

11
tests/lean/run/getArgPrime.lean Normal file
View file

@ -0,0 +1,11 @@
import Lean.Expr
open Lean Expr
example :
getArg! (mkApp (.mdata .empty (mkApp (mkConst ``Nat.add) (mkNatLit 1))) (mkNatLit 2)) 0
= mkNatLit 2 := rfl
example :
getArg!' (mkApp (.mdata .empty (mkApp (mkConst ``Nat.add) (mkNatLit 1))) (mkNatLit 2)) 0
= mkNatLit 1 := rfl