Commit 2022-10-22 17:27 66827114

View on Github →

feat: port choose (#420)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Expr.addLocalVarInfoForBinderIdent

added def Lean.Expr.getBinderName

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Choose.lean

added def Mathlib.Tactic.Choose.ElimStatus.merge

added inductive Mathlib.Tactic.Choose.ElimStatus

added def Mathlib.Tactic.Choose.choose1

added def Mathlib.Tactic.Choose.choose1WithInfo

added def Mathlib.Tactic.Choose.elabChoose

added def Mathlib.Tactic.Choose.mkFreshNameFrom

added def Mathlib.Tactic.Choose.mk_sometimes

Created test/choose.lean