Lean can convert between Bool and Prop? How?

Stream: lean4

[jim]

Hi all, I've noticed in a couple of places that Lean has some ability to convert between Bool and Prop, but I don't really understand what's going on.

Here's one place where Lean can convert a Prop to a Bool. This fails type-checking, as I would expect:

def foo1 : Bool := Nat.le 3 4

(It fails because it cannot unify Bool with Prop.) But then if I write:

def foo2 : Bool := LE.le 3 4

This type-checks! Even though LE.le: α → α → Prop, and is defined to be Nat.le on Nat. So ... is there something special about LE that lets Lean do this?

In the other direction, it seems Bool can sometimes be converted to Prop. For example I can write:

theorem three_is_three : (n: Nat) -> n = 3 -> n == 3 := by
  intro n hn
  rw [hn]
  simp

Here, n == 3 is somehow converted to (n == 3) = true. Again, I'm not sure what rules are being followed to allow this.

Sorry - I don't know what to call this feature, so I haven't been able to find out more about it ...

[Reid Barton]

There's a type class Decidable which is responsible for making this kind of coercion work, and there's probably no instance for Nat.le because you're not really supposed to ever write Nat.le.