mkApp for implicit arguments

Stream: general

[Frederick Pu]

Is there any any way to apply and expression (f : Expr) to an expression (e : Expr) while automatically infer all of the implicit arugments?

[Eric Wieser]

If you're using Qq, then this is q($f $e)

[Markus Himmel]

There is also docs#Lean.Meta.mkAppM

[Frederick Pu]

another question, you can pretty print exprs using Lean.Meta.ppExpr but is there any way to make it take macros into account. For example right now it pretty prints as Nat.add 10 15 can i make it pretty print as 10 + 15 instead?

[Eric Wieser]

Do you have a mwe? Usually those are different expressions, so them printing differently is a feature

[Frederick Pu]

Eric Wieser said:

Do you have a mwe? Usually those are different expressions, so them printing differently is a feature

Sorry for the late reply, I've been dreading trying to explain what I'm doing.

So, I'm making a tactic called cumulative that basically adds together all functions with a particular labell attribute.

/--
  `cumulative attr of x` exacts the sum of all functions with label attribute `attr` applied to `x`

  For instance suppose the only function with attr `tax_code` are:
  ```
    @[tax_code]
    def f₁ {α : Type*} [Semiring α] (a : α) : Nat := ...

    @[tax_code]
    def f₂ {α : Type*} [AddCommMonoid α] (a : α) : Nat := ...
  ```
  Then giving `α : Type*` satisfies enough typeclasses instances,
  for any `a : α`, `cumulative tax_code of a` is equivalent to `exact List.sum [f₁ a, f₂ a]`
-/
syntax (name := cumulative) "cumulative " ident "of" term : tactic

Right now, I've switched to using List.sum, since List.cons a (List.cons b List.nil) automatically pretty prints as [a, b]. But I'm open to other options.

If I use Qq, will the expression be pretty printed in it's un elaborated form a + b + c, because for some reason even Add.add a b doesn't pretty print as a + b

[Kyle Miller]

Could you say more about what your concerns are regarding pretty printing? Is it that you want it to be in the right form inside the goal window?

[Frederick Pu]

yes in the form a exact try this suggestion

[Kyle Miller]

If you want a try this suggestion, then you don't need to elaborate, you can use syntax quotations. Is the intent that you want this to only be for try this?

[Kyle Miller]

In Mathlib/foo2.lean

import Lean

/-- Some label attribute -/
register_label_attr tax_code

In Mathlib/foo.lean

import Mathlib.foo2
import Mathlib

@[tax_code]
def f₁ {α : Type*} [Semiring α] (a : α) : Nat := 2

@[tax_code]
def f₂ {α : Type*} [AddCommMonoid α] (a : α) : Nat := 3

open Lean Elab

elab tk:"cumulative " id:ident " of " t:term : tactic => do
  let names ← labelled id.getId
  let applied ← names.mapM fun n => `($(mkIdent n) $t)
  let term : Term ←
    if applied.isEmpty then
      `(0)
    else
      applied.foldlM (init := applied[0]!) (start := 1) fun stx app => `($stx + $app)
  let tac ← `(tactic| let $(mkIdent `val) := $term)
  Tactic.evalTactic tac
  Meta.Tactic.TryThis.addSuggestion tk tac (origSpan? := ← getRef)

/--
info: Try this: let val := f₁ a + f₂ a
---
error: unsolved goals
a : ℝ
val : ℕ := f₁ a + f₂ a
⊢ False
-/
#guard_msgs in
example (a : ℝ) : False := by
  cumulative tax_code of a

[Kyle Miller]

for some reason even Add.add a b doesn't pretty print as a + b

Only HAdd.hAdd pretty prints as a + b.