Documentation Verification Report

CollectFacts

📁 Source: Mathlib/Tactic/Order/CollectFacts.lean

Statistics

Metric	Count
Definitions `AtomicFact`, `CollectFactsM`, `CollectFactsState`, `addAtom`, `addFact`, `addType`, `collectFacts`, `collectFactsImp`, `instBEqAtomicFact`, `beq`, `instInhabitedAtomicFact`, `default`, `instToStringAtomicFact`	13
Theorems	0
Total	13

Mathlib.Tactic.Order

Definitions

Name	Category	Theorems
`AtomicFact` 📖	CompData	—
`CollectFactsM` 📖	CompOp	—
`CollectFactsState` 📖	CompOp	—
`addAtom` 📖	CompOp	—
`addFact` 📖	CompOp	—
`addType` 📖	CompOp	—
`collectFacts` 📖	CompOp	—
`collectFactsImp` 📖	CompOp	—
`instBEqAtomicFact` 📖	CompOp	—
`instInhabitedAtomicFact` 📖	CompOp	—
`instToStringAtomicFact` 📖	CompOp	—

Mathlib.Tactic.Order.instBEqAtomicFact

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Mathlib.Tactic.Order.instInhabitedAtomicFact

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index