Zulip Chat Archive
Stream: general
Topic: mkApp for implicit arguments
Frederick Pu (Apr 28 2024 at 14:43):
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 (Apr 28 2024 at 14:53):
If you're using Qq, then this is q($f $e)
Markus Himmel (Apr 28 2024 at 14:56):
There is also docs#Lean.Meta.mkAppM
Frederick Pu (Apr 28 2024 at 15:24):
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 (Apr 28 2024 at 15:48):
Do you have a mwe? Usually those are different expressions, so them printing differently is a feature
Frederick Pu (Apr 29 2024 at 23:00):
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 (Apr 29 2024 at 23:24):
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 (Apr 29 2024 at 23:44):
yes in the form a exact try this suggestion
Kyle Miller (Apr 30 2024 at 00:03):
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 (Apr 30 2024 at 00:15):
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 (Apr 30 2024 at 00:16):
for some reason even
Add.add a b
doesn't pretty print asa + b
Only HAdd.hAdd
pretty prints as a + b
.
Last updated: May 02 2025 at 03:31 UTC