## Stream: new members

### Topic: Lean displaying _ in local context

#### Keefer Rowan (May 20 2020 at 22:08):

I can't come up with a simpler example of this phenomenon, so I can only give you a slightly convoluted one. A complicated function I defined has one of its equations printed by Lean (by the #print command) as

set.subset_of_sts_all_less_than_finite_func.equations._eqn_2 : ∀ {n : ℕ} (m : ℕ) (A : set (all_less_than n).set_to_subtype)
(h : A.subset_of_sts_all_less_than_finite_size_of = m.succ) (x_val : (all_less_than n).set_to_subtype)
(x_property : x_val ∈ A),
subset_of_sts_all_less_than_finite_func h ⟨x_val, x_property⟩ =
dite (x_val = classical.some _) (λ (hyp : x_val = classical.some _), ⟨m, _⟩)
(λ (hyp : ¬x_val = classical.some _), ⟨(subset_of_sts_all_less_than_finite_func _ ⟨x_val, _⟩).val, _⟩)


Note the _. These terms are fairly complicated and it doesn't seem like they can be inferred from the local context, so I'm confused as to why Lean represents them with _. Is this a a printing option?

My problem is that these _'s propagate when trying to prove stuff about my definition, making it hard to complete proofs as an important part of the definition is just given as _.

#### Keefer Rowan (May 20 2020 at 22:13):

As an example of the problem I'm having, I have this in my local context,

h : ⟨m, _⟩ = ⟨(subset_of_sts_all_less_than_finite_func _ ⟨y_val, _⟩).val, _⟩


but rw subtype.mk.inj_eq at h, fails as rewrite tactic failed, did not find instance of the pattern in the target expression ⟨?m_3, ?m_4⟩ = ⟨?m_5, ?m_6⟩, which doesn't make any sense, but I'm assuming it has something to do with the _'s.

#### Anas Himmi (May 20 2020 at 22:14):

try putting

set_option pp.implicit  true


it may show you what's wrong

#### Alex J. Best (May 20 2020 at 22:14):

It's because they are proofs (so terms whose type is a Prop) so any two proofs of the same prop are equal, hence sometimes not that relevant to see them all the time, this can be controlled with set_option pp.proofs true

#### Alex J. Best (May 20 2020 at 22:14):

set_option pp.proofs true
noncomputable theory
lemma t : classical.some (⟨1, dec_trivial⟩: ∃ p, 0 < p) = 2 := sorry
#print t


#### Keefer Rowan (May 20 2020 at 22:20):

Any idea why rw subtype.mk.inj_eq at h isn't working?

#### Alex J. Best (May 20 2020 at 22:24):

Not without a #mwe ;)

Last updated: Dec 20 2023 at 11:08 UTC