Def Mathlib.Tactic.Choose.parseChooseArg

Modification history

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