Zulip Chat Archive

Stream: new members

Topic: reduction in the error message


view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 30 2019 at 15:47):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 30 2019 at 17:17):

use begin dsimp [bool_to_prop], end

view this post on Zulip Gun Pinyo (May 30 2019 at 17:23):

Sorry, but it doesn't work.

view this post on Zulip Gun Pinyo (May 30 2019 at 17:24):

Ok, I mistake, it works.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 30 2019 at 17:46):

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

view this post on Zulip Mario Carneiro (May 30 2019 at 17:46):

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

view this post on Zulip 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

view this post on Zulip Gun Pinyo (May 30 2019 at 17:56):

Thank you so much for your help :)


Last updated: May 10 2021 at 16:20 UTC