# Zulip Chat Archive

## Stream: new members

### Topic: Boolean equality on nats

#### Donald Sebastian Leung (Feb 22 2020 at 06:04):

In the Coq standard library, there is a boolean test for equality on the natural numbers `n =? m`

which returns true if `n`

and `m`

are equal and false otherwise. Is there a similar function in Lean?

On the other hand, I found `nat.decidable_eq`

in the Lean stdlib which I presume is analogous to Coq's sumbool. In Coq, we can convert it into a boolean by placing it in an if/then/else as follows (assuming `eq_dec`

is our sumbool instance): `if eq_dec then true else false`

. Is there a similar mechanism in Lean?

#### Donald Sebastian Leung (Feb 22 2020 at 06:12):

Donald Sebastian Leung said:

In the Coq standard library, there is a boolean test for equality on the natural numbers

`n =? m`

which returns true if`n`

and`m`

are equal and false otherwise. Is there a similar function in Lean?On the other hand, I found

`nat.decidable_eq`

in the Lean stdlib which I presume is analogous to Coq's sumbool. In Coq, we can convert it into a boolean by placing it in an if/then/else as follows (assuming`eq_dec`

is our sumbool instance):`if eq_dec then true else false`

. Is there a similar mechanism in Lean?

I skipped to Chapter 10 and found that you could pattern-match on `nat.decidable_eq n m`

(for some `n m : ℕ`

)

#### Bryan Gin-ge Chen (Feb 22 2020 at 06:46):

In Lean, you can use `if ... then ... else`

on `decidable`

`Prop`

s like this:

def foo (m n : ℕ) : bool := if m = n then tt else ff #eval foo 2 3

You can also coerce `decidable`

`Prop`

s to `bool`

s:

#eval (2 = 3 : bool) def foo' (m n : ℕ) : bool := m = n #print foo' -- `to_bool` is inserted

#### Donald Sebastian Leung (Feb 22 2020 at 06:47):

Thanks!

Last updated: May 13 2021 at 22:15 UTC