## Stream: general

### Topic: enforcing a type with show

#### Sebastien Gouezel (Sep 24 2020 at 08:57):

Sometimes, you want to tell Lean that a term has some type, but even type annotations are not enough because Lean sees them but it discards them right away as it has its own opinion on what the type is, so why should it listen to you. I've just seen a trick in Yury's PR #4199 where Lean has no choice but listen to you. Maybe it's a standard trick, but it was new to me so I thought I could share it here. The idea is to first give the type with show, and then the term:

theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
set.range (show ℕ → α, from λ n, nat.rec x f n) =
{x} ∪ set.range (λ n, nat.rec (f 0 x) (f ∘ succ) n) :=


Lean is happy with this, while I don't know how to make it happy only with type annotations.

#### Sebastien Gouezel (Sep 24 2020 at 09:00):

In fact, I can do it with type annotations:

theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
(set.range (λ n, nat.rec x f n) : set α) =
{x} ∪ set.range (λ n, nat.rec (f 0 x) (f ∘ succ) n) :=


But still it's a good trick to know.

#### Mario Carneiro (Sep 24 2020 at 14:40):

Note that show leaves "junk" (an identity function) in the term, unlike type annotations. This is actually the reason behind the difference in behavior

#### Mario Carneiro (Sep 24 2020 at 14:41):

so you should be careful doing this in things like simp lemmas

Last updated: May 09 2021 at 20:11 UTC