# Zulip Chat Archive

## Stream: new members

### Topic: Is it bug?

#### Anton Kalsin (Jan 21 2020 at 00:04):

Sorry for my english.

I've placed questions in code. What is going on? Can anybody explain me?

namespace hidden universe u inductive eq {α : Type u} (a : α) : α → Prop | refl : eq a @[elab_as_eliminator] theorem subst {α : Type u} {a b : α} {P : α → Prop} (h₁ : eq a b) (h₂ : P a) : P b := eq.rec h₂ h₁ def subst₂ {α : Type u} {a b : α} (P : α → Prop) (h₁ : eq a b) (h₂ : P a) : P b := @subst α a b P h₁ h₂ example {α β : Type u} {a b : α} (f : α → β) (h : eq a b) : eq (f a) (f b) := have p : α → Prop, from assume x, eq (f a) (f x), -- why₁? have (λ x, eq (f a) (f x)) a = eq (f a) (f a), from rfl, -- it's ok --have p a = eq (f a) (f a), from rfl, -- it's not ok sorry example {α β : Type u} {a b : α} (f : α → β) (h : eq a b) : eq (f a) (f b) := let p : α → Prop := λ x, eq (f a) (f x) in have e : p a, from eq.refl (f a), -- why₂? have @subst α a b p h e = subst₂ p h e, from rfl, -- have this, but: show eq (f a) (f b), from @subst α a b p h e -- it's ok --show eq (f a) (f b), from subst₂ p h e -- it's not ok end hidden

#### Kevin Buzzard (Jan 21 2020 at 00:06):

Try the more modern web editor at https://leanprover-community.github.io/lean-web-editor/ and see if anything changes?

#### Kevin Buzzard (Jan 21 2020 at 00:06):

That's running 3.5.0c

#### Anton Kalsin (Jan 21 2020 at 00:08):

No changes

#### Mario Carneiro (Jan 21 2020 at 00:09):

For `why₁`

, you need to use `let p : α → Prop := assume x, eq (f a) (f x),`

instead of `have`

#### Mario Carneiro (Jan 21 2020 at 00:09):

The difference is that with `let`

lean will remember the definition and be able to unfold it later

#### Anton Kalsin (Jan 21 2020 at 00:12):

Thanks. It's work

#### Mario Carneiro (Jan 21 2020 at 00:13):

For `why₂`

, the difference is that `subst₂`

is not marked as `elab_as_eliminator`

, so when it tries to figure out why `P b`

in the type of `subst₂`

should match with `eq (f a) (f b)`

it guesses `P := eq (f a)`

and `b := f b`

and gets to nonsense

#### Mario Carneiro (Jan 21 2020 at 00:13):

If you use `@subst₂ ...`

it should work

#### Mario Carneiro (Jan 21 2020 at 00:15):

Actually, for `elab_as_eliminator`

to work `b`

has to be explicit and provided

#### Mario Carneiro (Jan 21 2020 at 00:15):

so that it knows what to abstract

#### Anton Kalsin (Jan 21 2020 at 00:24):

Thanks. It's not clear for me now, but I'll read tutorial in more detail

#### Mario Carneiro (Jan 21 2020 at 00:31):

It's not really a theory thing, it has to do with how elaboration works. As long as you sprinkle enough `@`

signs you can make it work

Last updated: May 11 2021 at 12:15 UTC