Zulip Chat Archive
Stream: general
Topic: Explicitly naming case hypotheses in Lean 4
Arnav Sabharwal (Feb 16 2024 at 01:14):
Is there a way to name explicitly name all hypothesis generated by the 'cases' tactic? Thanks!
Shreyas Srinivas (Feb 16 2024 at 01:16):
Yes. cases <name>:<object>
Last updated: May 02 2025 at 03:31 UTC