Documentation Verification Report

Rule

📁 Source: Aesop/Rule.lean

Statistics

MetricCount
DefinitionsLocalNormSimpRule, id, instBEq, instHashable, name, simpTheorem, NormRule, NormRuleInfo, penalty, NormSimpRule, entries, instBEq, instHashable, name, RegularRule, indexingMode, instToFormat, isSafe, isUnsafe, name, successProbability, tac, withRule, Rule, SafeRule, SafeRuleInfo, penalty, safety, Safety, instToString, UnfoldRule, decl, instBEq, instHashable, name, unfoldThm?, UnsafeRule, UnsafeRuleInfo, successProbability, defaultNormPenalty, defaultSafePenalty, defaultSimpRulePriority, defaultSuccessProbability, instBEqRegularRule, beq, instInhabitedLocalNormSimpRule, default, instInhabitedNormRuleInfo, default, instInhabitedNormSimpRule, default, instInhabitedRegularRule, default, instInhabitedSafeRuleInfo, default, instInhabitedSafety, default, instInhabitedUnfoldRule, default, instInhabitedUnsafeRuleInfo, default, instLENormRuleInfo, instLESafeRuleInfo, instLEUnsafeRuleInfo, instLTNormRuleInfo, instLTSafeRuleInfo, instLTUnsafeRuleInfo, instOrdNormRuleInfo, instOrdSafeRuleInfo, instOrdUnsafeRuleInfo, instToStringNormRule, instToStringSafeRule, instToStringUnsafeRule
73
Theorems0
Total73

Aesop

Definitions

NameCategoryTheorems
LocalNormSimpRule 📖CompData
NormRule 📖CompOp
NormRuleInfo 📖CompData
NormSimpRule 📖CompData
RegularRule 📖CompData
Rule 📖CompData
SafeRule 📖CompOp
SafeRuleInfo 📖CompData
Safety 📖CompData
UnfoldRule 📖CompData
UnsafeRule 📖CompOp
UnsafeRuleInfo 📖CompData
defaultNormPenalty 📖CompOp
defaultSafePenalty 📖CompOp
defaultSimpRulePriority 📖CompOp
defaultSuccessProbability 📖CompOp
instBEqRegularRule 📖CompOp
instInhabitedLocalNormSimpRule 📖CompOp
instInhabitedNormRuleInfo 📖CompOp
instInhabitedNormSimpRule 📖CompOp
instInhabitedRegularRule 📖CompOp
instInhabitedSafeRuleInfo 📖CompOp
instInhabitedSafety 📖CompOp
instInhabitedUnfoldRule 📖CompOp
instInhabitedUnsafeRuleInfo 📖CompOp
instLENormRuleInfo 📖CompOp
instLESafeRuleInfo 📖CompOp
instLEUnsafeRuleInfo 📖CompOp
instLTNormRuleInfo 📖CompOp
instLTSafeRuleInfo 📖CompOp
instLTUnsafeRuleInfo 📖CompOp
instOrdNormRuleInfo 📖CompOp
instOrdSafeRuleInfo 📖CompOp
instOrdUnsafeRuleInfo 📖CompOp
instToStringNormRule 📖CompOp
instToStringSafeRule 📖CompOp
instToStringUnsafeRule 📖CompOp

Aesop.LocalNormSimpRule

Definitions

NameCategoryTheorems
id 📖CompOp
instBEq 📖CompOp
instHashable 📖CompOp
name 📖CompOp
simpTheorem 📖CompOp

Aesop.NormRuleInfo

Definitions

NameCategoryTheorems
penalty 📖CompOp

Aesop.NormSimpRule

Definitions

NameCategoryTheorems
entries 📖CompOp
instBEq 📖CompOp
instHashable 📖CompOp
name 📖CompOp

Aesop.RegularRule

Definitions

NameCategoryTheorems
indexingMode 📖CompOp
instToFormat 📖CompOp
isSafe 📖CompOp
isUnsafe 📖CompOp
name 📖CompOp
successProbability 📖CompOp
tac 📖CompOp
withRule 📖CompOp

Aesop.SafeRuleInfo

Definitions

NameCategoryTheorems
penalty 📖CompOp
safety 📖CompOp

Aesop.Safety

Definitions

NameCategoryTheorems
instToString 📖CompOp

Aesop.UnfoldRule

Definitions

NameCategoryTheorems
decl 📖CompOp
instBEq 📖CompOp
instHashable 📖CompOp
name 📖CompOp
unfoldThm? 📖CompOp

Aesop.UnsafeRuleInfo

Definitions

NameCategoryTheorems
successProbability 📖CompOp

Aesop.instBEqRegularRule

Definitions

NameCategoryTheorems
beq 📖CompOp

Aesop.instInhabitedLocalNormSimpRule

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedNormRuleInfo

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedNormSimpRule

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedRegularRule

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedSafeRuleInfo

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedSafety

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedUnfoldRule

Definitions

NameCategoryTheorems
default 📖CompOp

Aesop.instInhabitedUnsafeRuleInfo

Definitions

NameCategoryTheorems
default 📖CompOp

---

← Back to Index