Holes in Lean

Stream: general

[Patrick Stevens]

Last noob question of the night from me: "holes" in Lean are not the same thing as holes in Agda, right? Agda lets you use the question mark symbol to create what they call a "hole", which is a subgoal; the prover can take a guess at how to fill if you ask it. I found http://leodemoura.github.io/files/lean_cade25.pdf which suggests that the underscore should do something similar in Lean, but my feeble attempts with the underscore and with curly braces don't seem to replicate what Agda does.

[Kenny Lau]

in tactic mode you can do refine, which makes _ into subgoals

[Kenny Lau]

in term mode subgoals don't make sense

[Kenny Lau]

the syntax of refine is similar to exact

[Patrick Stevens]

Great, thanks - I'll have a play with it now I know what I'm looking for

[Andrew Ashworth]

Holes in Lean are an incomplete alpha feature, the syntax is {! !}. They aren't so useful right now

[Kenny Lau]

@Andrew Ashworth is that different from refine funext _?

[Andrew Ashworth]

yes

[Andrew Ashworth]

holes are a way to make term mode as easy to use as tactics, in a way. stuff like automatically knowing the type of a hole, and clicking an option to write out a match statement, or calc block, generally any sequence of term mode steps that can be automated

[Andrew Ashworth]

but yeah, it's sorta like _, but better

[Andrew Ashworth]

I'm not sure why it needs a special syntax, I'm not too familiar with holes. They are big in Agda and Idris

[Kevin Buzzard]

I see holes all the time in tactic mode. I try and make my tactic proof run at all times, and fill the holes with sorry, and then sometimes remove one and just look at the output to see what I have to fill. It's so much easier in tactic mode which is why I use tactic mode for anything non-trivial basically