Boolean equality on nats

Stream: new members

[Donald Sebastian Leung]

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]

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]

In Lean, you can use if ... then ... else on decidable Props like this:

def foo (m n : ℕ) : bool := if m = n then tt else ff

#eval foo 2 3

You can also coerce decidable Props to bools:

#eval (2 = 3 : bool)

def foo' (m n : ℕ) : bool := m = n

#print foo' -- `to_bool` is inserted

[Donald Sebastian Leung]

Thanks!