name of coercion

Stream: lean4

[Kevin Buzzard]

How do I see the name of a coercion in Lean 4?

def foo (b : Bool) : Prop := b

#print foo
/-
def foo : Bool → Prop :=
fun b => b = true
-/

def bar : CoeSort Bool Prop := inferInstance
#print bar -- it's `inferInstance`

I know there's a coercion from Bool to Prop but I would like to find it in the source code. Note that I am not asking "where is this specific coercion defined", I am asking "what is the algorithm for answering all questions of this nature".

Here's how I do it in Lean 3:

import tactic

example : has_coe_to_sort bool Prop := by show_term {apply_instance}
/-
Try this: exact coe_sort_bool
-/

[Mario Carneiro]

#synth is the command for this

[Kevin Buzzard]

oh nice -- thanks.

[Gabriel Ebner]

I often do:

variable (b : Bool) in
#check (b : Prop)

[Joseph Myers]

All these sorts of translations between Lean 3 and Lean 4 tricks are among the things that need to go in a migration guide (I imagine a table listing examples of Lean 3 constructs - including mathlib and leanproject commands - with brief summaries of what they do, and then giving a Lean 4 equivalent), rather than being lost in random Zulip threads.

[Scott Morrison]

@Joseph Myers, while the wheels turn towards a proper migration guide, I've been dumping somethings into https://github.com/leanprover-community/mathlib4/wiki, in particular the Some common fixes section. I've just added this one, but hopefully everyone can pile in. It's not a long term document, but hopefully it can help prevent tricks being lost.