reduction in the error message

Stream: new members

[Gun Pinyo]

Hi everybody, I have some question regarding error message to ask.

When we have a hole, we can change it to just "_" so make lean report context and the type of the missing hole.
The problem is that the type there is not reduce at all. Do you know how can I make lean reduce such the type?

FYI: I have tried
set_option pp.beta true
but it doesn't work

[Mario Carneiro]

what kind of reduction? What you see is what lean expects

[Gun Pinyo]

For example, if I have the following code

def bool_to_prop : bool → Prop
| ff := false
| tt := true

example : Π (b : bool), bool_to_prop b
| ff := _
| tt := _ -- cursor is at this underscore

when I place the cursor at the underscore of the last line I get a message

don't know how to synthesize placeholder
context:
_example : ∀ (b : bool), bool_to_prop b
⊢ bool_to_prop tt

I would like bool_to_prop tt to reduce and show just true

[Mario Carneiro]

use begin dsimp [bool_to_prop], end

[Gun Pinyo]

Sorry, but it doesn't work.

[Gun Pinyo]

Ok, I mistake, it works.

[Gun Pinyo]

Anyway, rather than stating the function explicitly. I would like to reduce the main goal into its normal form. Can I use dsimp to do it?

[Mario Carneiro]

dsimp would do it if you marked the function as @[simp]

[Mario Carneiro]

in general unfolding all definitions is a bad idea and can take a very long time

[Mario Carneiro]

there is a low level tactic called whnf that will do this, at least at the head of the expression

[Gun Pinyo]

Thank you so much for your help :)