Zulip Chat Archive
Stream: lean4
Topic: Extract function
Patrick Massot (Feb 14 2024 at 20:36):
It would be nice to have a version of docs#Mathlib.Tactic.ExtractGoal.extractGoal that works in do notation when programming.
Mario Carneiro (Feb 15 2024 at 02:58):
I guess that would just be a term mode version of it, which would work in both do notation and in arbitrary subterms
Mario Carneiro (Feb 15 2024 at 02:58):
show_term does something similar
Last updated: May 02 2025 at 03:31 UTC