## Stream: new members

### Topic: reduction in the error message

#### Gun Pinyo (May 30 2019 at 15:36):

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 (May 30 2019 at 15:47):

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

#### Gun Pinyo (May 30 2019 at 17:16):

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 (May 30 2019 at 17:17):

use begin dsimp [bool_to_prop], end

#### Gun Pinyo (May 30 2019 at 17:23):

Sorry, but it doesn't work.

#### Gun Pinyo (May 30 2019 at 17:24):

Ok, I mistake, it works.

#### Gun Pinyo (May 30 2019 at 17:29):

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 (May 30 2019 at 17:46):

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

#### Mario Carneiro (May 30 2019 at 17:46):

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

#### Mario Carneiro (May 30 2019 at 17:47):

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

#### Gun Pinyo (May 30 2019 at 17:56):

Thank you so much for your help :)

Last updated: May 10 2021 at 16:20 UTC