hole commands

Stream: general

[Johan Commelin]

One thing that might be of general interest that got some attention in Orsay: Lean has support for holes, but it isn't up to par to some other theorem provers. Nevertheless, try typing

import tactic.tidy

example : your_favourite_triviality := {! _ !}

and hit Ctrl-. (control-dot) while you are on the hole ({! _ !}). You will get a list of hole commands that are available. Three of them are somewhat silly, and one was added in Orsay: the tidy hole command. If your favourite triviality is actually Lean-trivial, then this hole-command will write a complete tactic proof for you.

[Johan Commelin]

It might be a good idea to think about other useful hole commands.

[Kenny Lau]

could you show us an example?

[Kenny Lau]

oh nvm I didn't import tactic.tidy