Documentation Verification Report

Modules

137 modules

ModuleDefinitionsTheoremsSorry
Aesop/BaseM.lean 10 0
Aesop/Builder/Apply.lean 6 0
Aesop/Builder/Basic.lean 33 0
Aesop/Builder/Cases.lean 9 0
Aesop/Builder/Constructors.lean 5 0
Aesop/Builder/Default.lean 1 0
Aesop/Builder/Forward.lean 7 0
Aesop/Builder/NormSimp.lean 3 0
Aesop/Builder/Tactic.lean 4 0
Aesop/Builder/Unfold.lean 4 0
Aesop/BuiltinRules.lean 0 4
Aesop/BuiltinRules/ApplyHyps.lean 2 0
Aesop/BuiltinRules/Assumption.lean 1 0
Aesop/BuiltinRules/DestructProducts.lean 2 0
Aesop/BuiltinRules/Ext.lean 2 0
Aesop/BuiltinRules/Intros.lean 1 0
Aesop/BuiltinRules/Rfl.lean 1 0
Aesop/BuiltinRules/Split.lean 3 0
Aesop/BuiltinRules/Subst.lean 6 0
Aesop/Check.lean 10 0
Aesop/Constants.lean 2 0
Aesop/EMap.lean 22 0
Aesop/ElabM.lean 12 0
Aesop/Exception.lean 1 0
Aesop/Forward/LevelIndex.lean 17 0
Aesop/Forward/Match.lean 18 0
Aesop/Forward/Match/Types.lean 33 0
Aesop/Forward/PremiseIndex.lean 17 0
Aesop/Forward/RuleInfo.lean 21 0
Aesop/Forward/SlotIndex.lean 19 0
Aesop/Forward/State.lean 115 1
Aesop/Forward/State/ApplyGoalDiff.lean 1 0
Aesop/Forward/State/Initial.lean 1 0
Aesop/Forward/State/UpdateGoal.lean 1 0
Aesop/Forward/Substitution.lean 19 0
Aesop/Frontend/Attribute.lean 10 0
Aesop/Frontend/Basic.lean 5 0
Aesop/Frontend/Command.lean 6 0
Aesop/Frontend/Extension.lean 15 0
Aesop/Frontend/Extension/Init.lean 10 0
Aesop/Frontend/RuleExpr.lean 116 0
Aesop/Frontend/Saturate.lean 21 0
Aesop/Frontend/Tactic.lean 23 0
Aesop/Index.lean 14 0
Aesop/Index/Basic.lean 23 0
Aesop/Index/DiscrTreeConfig.lean 4 0
Aesop/Index/Forward.lean 13 0
Aesop/Index/RulePattern.lean 24 0
Aesop/Main.lean 1 0
Aesop/Nanos.lean 17 0
Aesop/Options.lean 1 0
Aesop/Options/Internal.lean 7 0
Aesop/Options/Public.lean 37 0
Aesop/Percent.lean 17 0
Aesop/Rule.lean 73 0
Aesop/Rule/Basic.lean 15 0
Aesop/Rule/Forward.lean 22 0
Aesop/Rule/Name.lean 61 0
Aesop/RulePattern.lean 11 0
Aesop/RulePattern/Cache.lean 6 0
Aesop/RuleSet.lean 64 2
Aesop/RuleSet/Filter.lean 16 0
Aesop/RuleSet/Member.lean 13 0
Aesop/RuleSet/Name.lean 6 0
Aesop/RuleTac.lean 2 0
Aesop/RuleTac/Apply.lean 6 0
Aesop/RuleTac/Basic.lean 34 0
Aesop/RuleTac/Cases.lean 4 0
Aesop/RuleTac/Descr.lean 4 0
Aesop/RuleTac/ElabRuleTerm.lean 15 0
Aesop/RuleTac/FVarIdSubst.lean 19 0
Aesop/RuleTac/Forward.lean 20 0
Aesop/RuleTac/Forward/Basic.lean 14 0
Aesop/RuleTac/GoalDiff.lean 16 0
Aesop/RuleTac/Preprocess.lean 1 0
Aesop/RuleTac/RuleTerm.lean 12 0
Aesop/RuleTac/Tactic.lean 9 0
Aesop/Saturate.lean 13 0
Aesop/Script/Check.lean 2 0
Aesop/Script/CtorNames.lean 12 0
Aesop/Script/GoalWithMVars.lean 8 0
Aesop/Script/Main.lean 2 0
Aesop/Script/OptimizeSyntax.lean 3 0
Aesop/Script/SScript.lean 5 0
Aesop/Script/ScriptM.lean 7 0
Aesop/Script/SpecificTactics.lean 38 0
Aesop/Script/Step.lean 29 1
Aesop/Script/StructureDynamic.lean 14 0
Aesop/Script/StructureStatic.lean 7 0
Aesop/Script/Tactic.lean 11 0
Aesop/Script/TacticState.lean 15 0
Aesop/Script/UScript.lean 4 0
Aesop/Script/UScriptToSScript.lean 10 1
Aesop/Script/Util.lean 2 0
Aesop/Search/ExpandSafePrefix.lean 6 0
Aesop/Search/Expansion.lean 18 0
Aesop/Search/Expansion/Basic.lean 1 0
Aesop/Search/Expansion/Norm.lean 40 0
Aesop/Search/Expansion/Simp.lean 7 0
Aesop/Search/Main.lean 15 0
Aesop/Search/Queue.lean 28 0
Aesop/Search/Queue/Class.lean 4 0
Aesop/Search/RuleSelection.lean 4 0
Aesop/Search/SearchM.lean 35 1
Aesop/Stats/Basic.lean 110 0
Aesop/Stats/Extension.lean 14 0
Aesop/Stats/File.lean 11 0
Aesop/Stats/Report.lean 8 0
Aesop/Tracing.lean 38 0
Aesop/Tree.lean 1 0
Aesop/Tree/AddRapp.lean 12 0
Aesop/Tree/Check.lean 11 0
Aesop/Tree/Data.lean 247 6
Aesop/Tree/Data/ForwardRuleMatches.lean 20 0
Aesop/Tree/ExtractProof.lean 4 0
Aesop/Tree/ExtractScript.lean 18 0
Aesop/Tree/Free.lean 4 0
Aesop/Tree/RunMetaM.lean 13 0
Aesop/Tree/State.lean 33 0
Aesop/Tree/Stats.lean 3 0
Aesop/Tree/Tracing.lean 8 0
Aesop/Tree/Traversal.lean 7 0
Aesop/Tree/TreeM.lean 26 0
Aesop/Tree/UnsafeQueue.lean 18 0
Aesop/Util/Basic.lean 58 0
Aesop/Util/EqualUpToIds.lean 45 0
Aesop/Util/OrderedHashSet.lean 18 0
Aesop/Util/Tactic.lean 2 0
Aesop/Util/Tactic/Ext.lean 6 0
Aesop/Util/Tactic/Unfold.lean 2 0
Aesop/Util/Unfold.lean 6 0
Aesop/Util/UnionFind.lean 15 0
Aesop/Util/UnorderedArraySet.lean 33 0
AesopTest/LocalRuleSet.lean 1 0
AesopTest/Strategy.lean 1 0
AesopTest/TacGen.lean 1 0
AesopTest/TacticConfig.lean 1 0