Hint

📁 Source: Mathlib/Tactic/Hint.lean

Statistics

Metric	Count
Definitions addHint, getHints, hintExtension, hintStx, registerHintStx, suggestion	6
Theorems	0
Total	6

Mathlib.Tactic.Hint

Definitions

Name	Category	Theorems
addHint 📖	CompOp	—
getHints 📖	CompOp	—
hintExtension 📖	CompOp	—
hintStx 📖	CompOp	—
registerHintStx 📖	CompOp	—
suggestion 📖	CompOp	—

---

← Back to Index