Zulip Chat Archive

Stream: general

Topic: Holes in Lean


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

view this post on Zulip Kenny Lau (May 28 2018 at 22:15):

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

view this post on Zulip Kenny Lau (May 28 2018 at 22:15):

in term mode subgoals don't make sense

view this post on Zulip Kenny Lau (May 28 2018 at 22:16):

the syntax of refine is similar to exact

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

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

view this post on Zulip Kenny Lau (May 28 2018 at 22:26):

@Andrew Ashworth is that different from refine funext _?

view this post on Zulip Andrew Ashworth (May 28 2018 at 22:26):

yes

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

view this post on Zulip Andrew Ashworth (May 28 2018 at 22:30):

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

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

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