Implicit arguments in getAppArgs

Stream: lean4

[Moritz Doll]

Given variable {a b : ℕ} and the term a = b if I elaborate this term with elabTerm and then apply Lean.Expr.getAppArgs' (same for unprimed and the second component of Lean.Expr.getAppFnArgs) it yields #[ℕ, a, b], but I would expect #[a, b]. Is there some way to get rid of implicit arguments?

[Kyle Miller]

Are you specifically wanting to process equalities? docs4#Lean.Expr.eq? lets you get the type, LHS, and RHS as a tuple

[Moritz Doll]

Unfortunately not. Background is that I resumed porting congrm and for matching the pattern I of course only want to deal with the explicit arguments

[Kyle Miller]

I think there's a function used by other congr meta code to get detailed information about every function argument.

[Kyle Miller]

here's a place it's used in mathlib code: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Congr!.lean#LL540C16-L540C31

[Kyle Miller]

You can filter the arguments by which ones have a paramInfo.binderInfo == .default

[Moritz Doll]

thanks, there is actually ParamInfo.isExplicit

[Moritz Doll]

which does the exact equality check

[Moritz Doll]

Ok, making progress, but still not quite there. In the function below I consistently get that the length of pinfo is zero:

def _root_.Lean.Expr.getExplicitArgs (f : Expr) : MetaM (Array Expr) := do
  let args := f.getAppArgs
  let pinfo := (← Lean.Meta.getFunInfoNArgs f args.toList.length).paramInfo
  logInfo s!"all arguments: {← args.mapM ppExpr} and num patternInfos: {pinfo.toList.length}"
  return (pinfo.zip args).filterMap (λ arg => if arg.1.isExplicit then some arg.2 else none)

[Mario Carneiro]

#mwe

[Moritz Doll]

There you go:

import Lean.Meta.FunInfo
import Lean.Elab.Tactic

open Lean Parser Tactic Elab Tactic Meta

def _root_.Lean.Expr.getExplicitArgs (f : Expr) : MetaM (Array Expr) := do
  let args := f.getAppArgs
  let pinfo := (← Lean.Meta.getFunInfoNArgs f args.toList.length).paramInfo
  logInfo s!"all arguments: {← args.mapM ppExpr} and patternInfos: {pinfo.toList.length}"
  return (pinfo.zip args).filterMap (λ arg => if arg.1.isExplicit then some arg.2 else none)

syntax (name := prettyExpr) "prettyExpr " term : tactic

elab_rules : tactic | `(tactic| prettyExpr $expr:term) => withMainContext do
  let _foo ← (← elabTerm expr none).getExplicitArgs
  return

-- Testing for implicit arguments in function application
example (a b c : α) (h : b = c) : a = b ↔ a = c := by
  prettyExpr (_ = _)
  prettyExpr ((· = · ) _ _)
  prettyExpr (@Eq _ _)
  sorry

[Mario Carneiro]

looks like you need to pass the head of the function, that is f.getAppFn, to getFunInfoNArgs instead of f

[Moritz Doll]

yes that works, thanks. What is the reason for (_ = _) having three arguments, but ((· = · ) _ _) having two?

[Mario Carneiro]

the first one is @Eq _ _ _ and the second one is (fun x y => @Eq _ x y) _ _

[Kyle Miller]

Rather than args.toList.length you can do args.size. And just in case you ever need it (if you don't also need the array of arguments), there's Lean.Expr.getAppNumArgs.

[Moritz Doll]

I knew about getAppNumArgs, but not Array.size, thanks