Core
📁 Source: Mathlib/Tactic/FunProp/Core.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsapplyApplyRule, applyCompRule, applyConstRule, applyIdRule, applyMorRules, applyPiRule, applyTransitionRules, bvarAppCase, cacheFailure, cacheResult, constAppCase, funProp, fvarAppCase, getDeclTheorems, getLocalTheorems, letCase, removeArgRule, synthesizeArgs, synthesizeInstance, tryTheorem?, tryTheoremCore, tryTheoremWithHint?, tryTheorems | 23 |
| Theorems | 0 |
| Total | 23 |
Mathlib.Meta.FunProp
Definitions
| Name | Category | Theorems |
|---|---|---|
applyApplyRule 📖 | CompOp | — |
applyCompRule 📖 | CompOp | — |
applyConstRule 📖 | CompOp | — |
applyIdRule 📖 | CompOp | — |
applyMorRules 📖 | CompOp | — |
applyPiRule 📖 | CompOp | — |
applyTransitionRules 📖 | CompOp | — |
bvarAppCase 📖 | CompOp | — |
cacheFailure 📖 | CompOp | — |
cacheResult 📖 | CompOp | — |
constAppCase 📖 | CompOp | — |
funProp 📖 | CompOp | — |
fvarAppCase 📖 | CompOp | — |
getDeclTheorems 📖 | CompOp | — |
getLocalTheorems 📖 | CompOp | — |
letCase 📖 | CompOp | — |
removeArgRule 📖 | CompOp | — |
synthesizeArgs 📖 | CompOp | — |
synthesizeInstance 📖 | CompOp | — |
tryTheorem? 📖 | CompOp | — |
tryTheoremCore 📖 | CompOp | — |
tryTheoremWithHint? 📖 | CompOp | — |
tryTheorems 📖 | CompOp | — |
---