Skip to content

Modify isZero function pattern matching to use underscore to avoid unused variable warning #276

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
conor10 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Modify isZero function pattern matching to use underscore to avoid unused variable warning #276

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions book/FPLean/GettingToKnow/DatatypesPatterns.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ An example of a function that uses pattern matching is {anchorName isZero}`isZer
def isZero (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => false
| Nat.succ _ => false
```

The {kw}`match` expression is provided the function's argument {anchorName isZero}`n` for destructuring.
Expand All @@ -143,7 +143,7 @@ isZero Nat.zero
===>
match Nat.zero with
| Nat.zero => true
| Nat.succ k => false
| Nat.succ _ => false
===>
true
```
Expand All @@ -159,16 +159,16 @@ isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))
===>
match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
| Nat.zero => true
| Nat.succ k => false
| Nat.succ _ => false
===>
false
```
:::

The {anchorName isZero}`k` in the second branch of the pattern in {anchorName isZero}`isZero` is not decorative.
It makes the {anchorName isZero}`Nat` that is the argument to {anchorName isZero}`Nat.succ` visible, with the provided name.
That smaller number can then be used to compute the final result of the expression.

The {anchorName isZero}`_` in the second branch of the pattern in {anchorName isZero}`isZero` is a placeholder.
It represents the {anchorName isZero}`Nat` that is the argument to {anchorName isZero}`Nat.succ`.
As we don't need to compute using this value we use {anchorName isZero}`_` here.
If we wanted to compute a value with this argument, we could give it a name such as `k`.

:::paragraph
Just as the successor of some number $`n` is one greater than $`n` (that is, $`n + 1`), the predecessor of a number is one less than it.
Expand Down