## Stream: general

### Topic: Holes in Lean

#### Patrick Stevens (May 28 2018 at 22:15):

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 (May 28 2018 at 22:15):

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

#### Kenny Lau (May 28 2018 at 22:15):

in term mode subgoals don't make sense

#### Kenny Lau (May 28 2018 at 22:16):

the syntax of refine is similar to exact

#### Patrick Stevens (May 28 2018 at 22:17):

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

#### Andrew Ashworth (May 28 2018 at 22:25):

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

#### Kenny Lau (May 28 2018 at 22:26):

@Andrew Ashworth is that different from refine funext _?

yes

#### Andrew Ashworth (May 28 2018 at 22:28):

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 (May 28 2018 at 22:30):

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

#### Andrew Ashworth (May 28 2018 at 22:30):

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 (May 29 2018 at 22:41):

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

Last updated: May 13 2021 at 17:42 UTC