# Zulip Chat Archive

## Stream: lean4

### Topic: metavariables in lemma statements

#### Alexander Bentkamp (Jan 11 2021 at 18:02):

Just discovered an interesting difference between Lean 3 and 4. Lean 4 allows metavariables in lemma statements:

```
theorem one_plus_one : 1 + 1 = _ :=
show (1 + 1 = 2) by rfl
```

Lean 3 doesn't accept them:

```
lemma one_plus_one : 1 + 1 = _ := -- don't know how to synthesize placeholder context: ⊢ ℕ
show 1 + 1 = 2, by refl
```

#### Adam Topaz (Jan 11 2021 at 18:06):

Interesting... this work in lean3:

```
example : 1 + 1 = _ := show 1 + 1 = 2, by refl
```

#### Adam Topaz (Jan 11 2021 at 18:06):

Must be something about `lemma`

vs. `example`

#### Gabriel Ebner (Jan 11 2021 at 18:08):

Right. In Lean 3 the lemma statement is elaborated first, and the proof is elaborated separately. There are two reasons:

- The statement of a lemma shouldn't depend on its proof. (Otherwise you might accidentally prove something weaker than you want.)
- We want to check proofs in parallel. For this to work we need to know the theorem statement without elaborating the proof.

#### Eric Wieser (Jan 11 2021 at 23:03):

Does that make this a shortcoming in lean 4? And if so, is it by design, accident, or just low prioritization?

#### Leonardo de Moura (Jan 11 2021 at 23:56):

@Eric Wieser This part is still missing. That being said, the behavior will still be slightly different from Lean 3. Significant changes:

- We are removing unused
`variable`

s from`theorem`

s. So, the behavior here is similar to`def`

in Lean 3. - If the user provides the type in a
`def`

, we will ensure it doesn't contain metavariables before we elaborate its body as we do for`theorem`

in Lean 3.

The goal is to reduce the number of differences between `theorem`

and `def`

.

#### Leonardo de Moura (Jan 12 2021 at 00:50):

I just pushed https://github.com/leanprover/lean4/commit/36008271eacc7af3c22828c3d3238650349017d4 since this change may create compatibility issues in the future.

It ensures the header of a theorem must not contain metavariable (aka holes) before we elaborate its body/value. Same for `def`

when the type is explicitly provided. That is, we can still write

```
def inc x := x + 1
```

but the following is an error

```
def inc x : id _ := x+1
```

Last updated: May 18 2021 at 23:14 UTC