Zulip Chat Archive

Stream: general

Topic: Feature request: Extract goal ++

Adam Topaz (Jan 30 2022 at 16:45):

Idris has a nice feature where (in emacs) C-c C-e extracts a goal as a top-level definition, and replaces the current goal with a call to that new definition. We have something similar with extract_goal in mathlib. How hard would it be to extend extract_goal so that it automatically makes a top level def (with a sorry) and replaces the current goal with that def?

Adam Topaz (Jan 30 2022 at 16:47):

(I guess it would have to be a hole command?)

Andrew Yang (Jan 30 2022 at 16:51):

Is tactic.interactive.abstract what you want? The tactic description looks promising but I have never figured out how to make it work.

Adam Topaz (Jan 30 2022 at 17:05):

Maybe! I have never even heard of abstract...

Adam Topaz (Jan 30 2022 at 17:05):

I'll have to try it later.

Rob Lewis (Jan 30 2022 at 17:40):

I think Adam wants something that changes the source code, right? abstract can be useful but it just creates a new declaration under the hood. I think what you're describing is extract_goal plus VSCode support. This doesn't seem doable with the current Try this: or with hole commands.

Adam Topaz (Jan 30 2022 at 19:19):

So what is abstract actually useful for? For example, can it help with deterministic timeouts in long proofs?

Eric Rodriguez (Jan 30 2022 at 19:42):

I just tried this, and I think extract_goal uses pp instead of to_string so copy-pasting goals created by it doesn't usually work :/ is round-tripping easier in Lean4?

Last updated: Aug 03 2023 at 10:10 UTC