Difference between def and let

Stream: new members

[Lambert A'Campo]

What is the difference between let and def? For example I wanted in the whole file to have

def B : set V := closed_ball 0 1

but then in a later proof I use

intros x hx,

while showing that B is contained in something but it doesn't work. However, if I use let it does work.

[Mario Carneiro]

Let and def are morally similar but live in different syntactic classes. As for your particular example we need more context, preferably a MWE

[Lambert A'Campo]

What is a MWE?

[Johan Commelin]

minimal working example

[Lambert A'Campo]

Ok so here is a not quite minimal example and I don't understand why the declaration of the example has type problems.

variables
{V : Type*} [normed_group V] [complete_space V] [normed_space ℝ V]

def B' : set V := closed_ball 0 1

example : B' ⊆ ⋃ (a : V) (H : a ∈ B'), ball a 0.5 :=
begin
  sorry
end

[Chris Hughes]

MWE with imports

import analysis.normed_space.basic
open metric
variables
{V : Type*} [normed_group V] [complete_space V] [normed_space ℝ V]

def B' : set V := closed_ball 0 1

example : B' ⊆ ⋃ (a : V) (H : a ∈ B'), ball a 0.5 :=
begin
  sorry
end

The problem is that V is an implicit argument to B' and Lean cannot infer this argument

[Chris Hughes]

Writing a ∈ (B' : set V) fixes the problem.

[Lambert A'Campo]

Oh ok thank you!

[Reid Barton]

In particular, variables are not "fixed" throughout a section.