# Zulip Chat Archive

## Stream: general

### Topic: strange elaboration

#### Kenny Lau (Jun 10 2020 at 07:31):

```
import analysis.normed_space.basic
open_locale big_operators
variables {α : Type} [normed_group α] {t : finset α} {f : α → α}
-- ∀ (ε : ℝ), ε > 0 → ∥t.sum f∥ < ε
example : ∀ε > 0, ∥ t.sum f ∥ < ε := by skip
-- ∀ (ε : ℕ), ε > 0 → ∥∑ (i : α) in t, f i∥ < ↑ε
example : ∀ε > 0, ∥ (∑ i in t, f i) ∥ < ε := by skip
```

#### Kenny Lau (Jun 10 2020 at 07:31):

the epsilon in the second example is (wrongly) interpreted as a natural number

#### Kenny Lau (Jun 10 2020 at 07:32):

the notation is irrelevant:

```
-- ∀ (ε : ℕ), ε > 0 → ∥∑ (i : α) in t, f i∥ < ↑ε
example : ∀ε > 0, ∥ t.sum (λ i, f i) ∥ < ε := by skip
```

#### Kenny Lau (Jun 10 2020 at 07:34):

strangely enough the type is correct again if `> 0`

is removed:

```
import analysis.normed_space.basic
variables {α : Type} [normed_group α] {t : finset α} {f : α → α}
-- ∀ (ε : ℝ), ε > 0 → ∥t.sum f∥ < ε
example : ∀ε > 0, ∥ t.sum f ∥ < ε := by skip
-- ∀ (ε : ℝ), ∥t.sum (λ (i : α), f i)∥ < ε
example : ∀ε, ∥ t.sum (λ i, f i) ∥ < ε := by skip
-- INCORRECT
-- ∀ (ε : ℕ), ε > 0 → ∥t.sum (λ (i : α), f i)∥ < ↑ε
example : ∀ε > 0, ∥ t.sum (λ i, f i) ∥ < ε := by skip
```

#### Mario Carneiro (Jun 10 2020 at 08:03):

In what sense is it incorrect? It looks like lean was able to type it either way

#### Mario Carneiro (Jun 10 2020 at 08:03):

The `0`

is the source of the nat defaulting

#### Kenny Lau (Jun 10 2020 at 08:10):

@Mario Carneiro then why does it get elaborated as \R in the first example?

#### Kenny Lau (Jun 10 2020 at 08:10):

maybe not "incorrect" but rather "inconsistent"

#### Mario Carneiro (Jun 10 2020 at 08:11):

nat defaulting has always been a little weird, since it is somewhat outside the usual elaboration process. It happens "late" but it still has to trigger before type inference is complete

#### Kenny Lau (Jun 10 2020 at 08:11):

so should I change it to the longer form `\forall \e : \R, \e > 0 \to`

?

#### Kenny Lau (Jun 10 2020 at 08:11):

https://github.com/leanprover-community/mathlib/runs/756776916

#### Mario Carneiro (Jun 10 2020 at 08:11):

I've never really been convinced it is a good idea, but the original point was so that people could just write `#eval 1 + 1`

and get something sensible

#### Kenny Lau (Jun 10 2020 at 08:11):

https://github.com/leanprover-community/mathlib/pull/3014

#### Yury G. Kudryashov (Jun 10 2020 at 08:12):

AFAIR you can use `ε > (0 : real)`

.

#### Mario Carneiro (Jun 10 2020 at 08:13):

You can also .. ninja'd

#### Kenny Lau (Jun 10 2020 at 08:13):

oh

#### Mario Carneiro (Jun 10 2020 at 08:13):

we should make `∀(ε : ℝ) > 0,`

work

#### Mario Carneiro (Jun 10 2020 at 08:14):

it's a bit silly that you can't put a type ascription there

#### Kenny Lau (Jun 10 2020 at 08:15):

#lean4 ?

#### Mario Carneiro (Jun 10 2020 at 08:18):

3.x should be able to handle it without too much work

#### Mario Carneiro (Jun 10 2020 at 08:18):

although I'm not in a position to hack on lean ATM

Last updated: May 16 2021 at 21:11 UTC