In the section 1.5.1. covering structures and pattern matching, the definition for depth binds unused variables (h and w), triggering a Lean 4 linter warning (UnusedVariables)
Code:
```lean def depth (p : Point3D) : Float := match p with | { x := h, y := w, z := d } => d
There maybe, the unused variables can be written with an underscore, like _h and _w.
In the section 1.5.1. covering structures and pattern matching, the definition for
depthbinds unused variables (handw), triggering a Lean 4 linter warning (UnusedVariables)Code:
```lean def depth (p : Point3D) : Float := match p with | { x := h, y := w, z := d } => dThere maybe, the unused variables can be written with an underscore, like _h and _w.