implicit arguments

Stream: new members

[Adrian]

What is the difference between implicit arguments in {} vs implicit arguments in {{}} in Lean 4?

[Jeremy Teitelbaum]

Can one ask lean to show the choices it has made for implicit arguments?

[Yaël Dillies]

Click on the stuff in the infoview!

[Yaël Dillies]

Or maybe you want to see how a goal was closed?

[Jeremy Teitelbaum]

Yaël Dillies said:

Click on the stuff in the infoview!

If you have theorem blah {implicits} (explicits) : (conclusion) := function....
can you extract the implicit assignments?

[Arthur Paulino]

What do you mean "extract"? Just get to know them?

[Yaël Dillies]

You can always use show_term

[Arthur Paulino]

When I want to know Lean's final decision on what's implicit and what's explicit, I use #print blah

[Jeremy Teitelbaum]

Here's what I'm trying to understand. In the proof that equality is symmetric, we have this:

@[elab_as_eliminator, subst]
lemma eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
eq.rec h₂ h₁

infixr ` ▸ `:75 := eq.subst

@[trans] lemma eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
h₂ ▸ h₁

@[symm] lemma eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl

The predicate P is an implicit argument to the subst lemma. It's not given explicitly in the proofs of trans and symm. What, exactly,
has it inferred for P?

[Arthur Paulino]

In eq.trans it's calling eq.subst h₂ h₁. So h2 and h1 are the explicit arguments. It gets a bit confusing because h1 and h2 get interchanged on that call of eq.subst

[Jeremy Teitelbaum]

But to call eq.subst it needs to infer the predicate P, and that’s what is like to understand.

[Alex J. Best]

You can use

set_option pp.implicit true
set_option pp.notation false
#print eq.symm