Recurse

📁 Source: Mathlib/Util/AtomM/Recurse.lean

Statistics

Metric	Count
Definitions Config, contextual, red, zetaDelta, Context, ctx, simp, instBEqConfig, beq, instInhabitedConfig, default, instReprConfig, repr, RecurseM, run, onSubexpressions, recurse	17
Theorems	0
Total	17

Mathlib.Tactic.AtomM

Definitions

Name	Category	Theorems
RecurseM 📖	CompOp	—
onSubexpressions 📖	CompOp	—
recurse 📖	CompOp	—

Mathlib.Tactic.AtomM.Recurse

Definitions

Name	Category	Theorems
Config 📖	CompData	—
Context 📖	CompData	—
instBEqConfig 📖	CompOp	—
instInhabitedConfig 📖	CompOp	—
instReprConfig 📖	CompOp	—

Mathlib.Tactic.AtomM.Recurse.Config

Definitions

Name	Category	Theorems
contextual 📖	CompOp	—
red 📖	CompOp	—
zetaDelta 📖	CompOp	—

Mathlib.Tactic.AtomM.Recurse.Context

Definitions

Name	Category	Theorems
ctx 📖	CompOp	—
simp 📖	CompOp	—

Mathlib.Tactic.AtomM.Recurse.instBEqConfig

Definitions

Name	Category	Theorems
beq 📖	CompOp	—

Mathlib.Tactic.AtomM.Recurse.instInhabitedConfig

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Mathlib.Tactic.AtomM.Recurse.instReprConfig

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

Mathlib.Tactic.AtomM.RecurseM

Definitions

Name	Category	Theorems
run 📖	CompOp	—

---

← Back to Index