Structure Mathlib.Tactic.Choose.ChooseArg

Modification history

2026-01-19 10:42
Mathlib/Tactic/Choose.lean
feat(Tactic/Choose): add type annotation support (#33033) …
Added Mathlib.Tactic.Choose.ChooseArgView on Github →