Implicit Arguments in Rewrites

Stream: metaprogramming / tactics

[Harun Khan]

Hi, how do I skip over implicit arguments when using Lean.MVarId.Rewrite? In other words, what's the equivalent of an underscore when using therewrite tactic. I've been making fresh mvars to simulate underscores. For instance,

let m1 ← mkFreshExprMVar (Expr.const ``Nat [])

but this gets long and tedious really quickly. What's an alternative?

[Scott Morrison]

Do you know about mkAppM?

[Harun Khan]

Scott Morrison said:

Do you know about mkAppM?

Oh this is what I need! Thanks!