NotationClass

📁 Source: Mathlib/Tactic/Simps/NotationClass.lean

Statistics

Metric	Count
Definitions AutomaticProjectionData, className, findArgs, isNotation, copyFirst, copySecond, defaultfindArgs, findArgType, findCoercionArgs, findOneArgs, findZeroArgs, instInhabitedAutomaticProjectionData, default, notationClassAttr, nsmulArgs, zsmulArgs, notation_class	17
Theorems	0
Total	17

Simps

Definitions

Name	Category	Theorems
AutomaticProjectionData 📖	CompData	—
copyFirst 📖	CompOp	—
copySecond 📖	CompOp	—
defaultfindArgs 📖	CompOp	—
findArgType 📖	CompOp	—
findCoercionArgs 📖	CompOp	—
findOneArgs 📖	CompOp	—
findZeroArgs 📖	CompOp	—
instInhabitedAutomaticProjectionData 📖	CompOp	—
notationClassAttr 📖	CompOp	—
nsmulArgs 📖	CompOp	—
zsmulArgs 📖	CompOp	—

Simps.AutomaticProjectionData

Definitions

Name	Category	Theorems
className 📖	CompOp	—
findArgs 📖	CompOp	—
isNotation 📖	CompOp	—

Simps.instInhabitedAutomaticProjectionData

Definitions

Name	Category	Theorems
default 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
notation_class 📖	CompOp	—

---

← Back to Index