## Stream: general

### Topic: Auto param issue

#### Adam Topaz (Aug 15 2020 at 18:59):

Here's something strange:

import algebra

(thing : A)
(zero_add {x : A} : 0 + x = x . obviously)

(thing : A)
(zero_add : ∀ {x : A}, 0 + x = x . obviously)

instance bar {A : Type*} [ring A] : zero_add_eq_zero A :=
{ thing := 1,
zero_add := by tidy } -- Works

instance baz {A : Type*} [ring A] : zero_add_eq_zero' A :=
{ thing := 1 } -- Works

instance foo {A : Type*} [ring A] : zero_add_eq_zero A :=
{ thing := 1 } -- Fails

/-
invalid structure value { ... }, field 'zero_add' was not provided
-/


What's going on? (This came up as part of the discussion about #3762 )
Ping @Scott Morrison

#### Adam Topaz (Aug 15 2020 at 19:15):

It doesn't seem to be an issue with "obviously" itself:

meta def thing := [simp]

`