## Stream: new members

### Topic: implicit arguments

#### Adrian (Sep 05 2021 at 20:37):

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

#### Jeremy Teitelbaum (Jan 12 2022 at 21:42):

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

#### Yaël Dillies (Jan 12 2022 at 21:46):

Click on the stuff in the infoview!

#### Yaël Dillies (Jan 12 2022 at 21:49):

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

#### Jeremy Teitelbaum (Jan 12 2022 at 21:50):

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 (Jan 12 2022 at 21:51):

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

#### Yaël Dillies (Jan 12 2022 at 21:52):

You can always use show_term

#### Arthur Paulino (Jan 12 2022 at 21:53):

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

#### Jeremy Teitelbaum (Jan 12 2022 at 21:58):

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 (Jan 12 2022 at 22:05):

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 (Jan 12 2022 at 22:09):

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

#### Alex J. Best (Jan 12 2022 at 22:11):

You can use

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


Last updated: Dec 20 2023 at 11:08 UTC