16.3. Local Definitions
grind has two flags that control how it treats local definitions with Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let.
They are enabled by default, but duplicating the local definition's value can lead to the term exploding in size; consider disabling them when working with terms that contain many nested Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
lets.
-
zeta(defaulttrue) This controls whether
grindperforms ζ-reduction. Unless this flag is disabled, terms that contain aLean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` The *anaphoric let* `let := v` defines a variable called `this`.letare reduced before they are added to the whiteboard, so thatlet x := 5; x + xis reduced to5 + 5before further processing. If it is disabled, the term is not reduced.-
zetaDelta(defaulttrue) This flag controls whether
grindreplaces variables in terms that have local definitions in the context with their definitions.If a proof goal is
let x := 5; (x + x = 10), runningresults in a proof state in which the definition of
xis in the context:Running
All goals completed! 🐙succeeds, because5is substituted forx. Without thezetaDeltaflag, it fails.