auto trigger slim_check

Stream: general

[Asei Inoue]

I have an idea of new feature of ‘sorry’

slim_check is a good way to check if proposition can be true. But we often forget to run slim_check.
So it could be good to run slim_check automatically when we write sorry.

How about do you think?

[Kim Morrison]

It's a good idea, but also not a new one. :-)

[Kim Morrison]

There are a lot of user interface questions around it. It's potentially quite expensive, and users won't always want "active sorries".

[Kim Morrison]

Some of theorem proving languages already do this (I forget which?)

[Kim Morrison]

You might alternatively triggering things like this even without a sorry, but e.g. whenever there is an error about an unsolved goal.