Choose

📁 Source: Mathlib/Tactic/Choose.lean

Statistics

Metric	Count
Definitions ChooseArg, expectedType?, name, ref, ElimStatus, merge, choose1, choose1WithInfo, chooseBinder, elabChoose, instInhabitedChooseArg, default, mkFreshNameFrom, mk_sometimes, parseChooseArg, tacticChoose!___Using_	16
Theorems	0
Total	16

Mathlib.Tactic.Choose

Definitions

Name	Category	Theorems
ChooseArg 📖	CompData	—
ElimStatus 📖	CompData	—
choose1 📖	CompOp	—
choose1WithInfo 📖	CompOp	—
chooseBinder 📖	CompOp	—
elabChoose 📖	CompOp	—
instInhabitedChooseArg 📖	CompOp	—
mkFreshNameFrom 📖	CompOp	—
mk_sometimes 📖	CompOp	—
parseChooseArg 📖	CompOp	—
tacticChoose!___Using_ 📖	CompOp	—

Mathlib.Tactic.Choose.ChooseArg

Definitions

Name	Category	Theorems
expectedType? 📖	CompOp	—
name 📖	CompOp	—
ref 📖	CompOp	—

Mathlib.Tactic.Choose.ElimStatus

Definitions

Name	Category	Theorems
merge 📖	CompOp	—

Mathlib.Tactic.Choose.instInhabitedChooseArg

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index