Attr

📁 Source: Batteries/CodeAction/Attr.lean

Statistics

Metric	Count
Definitions TacticCodeAction, TacticCodeActionEntry, declName, tacticKinds, TacticCodeActions, insert, onAnyTactic, onTactic, TacticSeqCodeAction, instInhabitedTacticCodeActionEntry, default, instInhabitedTacticCodeActions, default, mkTacticCodeAction, mkTacticSeqCodeAction, tacticCodeActionExt, tacticSeqCodeActionExt, tactic_code_action	18
Theorems	0
Total	18

Batteries.CodeAction

Definitions

Name	Category	Theorems
TacticCodeAction 📖	CompOp	—
TacticCodeActionEntry 📖	CompData	—
TacticCodeActions 📖	CompData	—
TacticSeqCodeAction 📖	CompOp	—
instInhabitedTacticCodeActionEntry 📖	CompOp	—
instInhabitedTacticCodeActions 📖	CompOp	—
mkTacticCodeAction 📖	CompOp	—
mkTacticSeqCodeAction 📖	CompOp	—
tacticCodeActionExt 📖	CompOp	—
tacticSeqCodeActionExt 📖	CompOp	—
tactic_code_action 📖	CompOp	—

Batteries.CodeAction.TacticCodeActionEntry

Definitions

Name	Category	Theorems
declName 📖	CompOp	—
tacticKinds 📖	CompOp	—

Batteries.CodeAction.TacticCodeActions

Definitions

Name	Category	Theorems
insert 📖	CompOp	—
onAnyTactic 📖	CompOp	—
onTactic 📖	CompOp	—

Batteries.CodeAction.instInhabitedTacticCodeActionEntry

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Batteries.CodeAction.instInhabitedTacticCodeActions

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index