Data

Statistics

Metric	Count
Definitions `Goal`, `addedInIteration`, `children`, `currentGoal`, `currentGoalAndMetaState`, `depth`, `elim`, `failedRapps`, `firstProvenRapp?`, `forwardRuleMatches`, `forwardState`, `hasMVar`, `hasProvableRapp`, `hasSafeRapp`, `id`, `instBEq`, `instHashable`, `isActive`, `isExhausted`, `isForcedUnprovable`, `isIrrelevant`, `isNormal`, `isRoot`, `isUnsafeExhausted`, `lastExpandedInIteration`, `mk`, `modify`, `mvars`, `normalizationState`, `origin`, `originalGoalId`, `parent`, `parentMetaState`, `parentRapp?`, `postNormGoal?`, `postNormGoalAndMetaState?`, `preNormGoal`, `priority`, `safeRapps`, `setAddedInIteration`, `setChildren`, `setDepth`, `setFailedRapps`, `setForwardRuleMatches`, `setForwardState`, `setId`, `setIsForcedUnprovable`, `setIsIrrelevant`, `setLastExpandedInIteration`, `setMVars`, `setNormalizationState`, `setOrigin`, `setParent`, `setPreNormGoal`, `setState`, `setSuccessProbability`, `setUnsafeQueue`, `setUnsafeRulesSelected`, `state`, `successProbability`, `unsafeQueue`, `unsafeQueue?`, `unsafeRulesSelected`, `GoalData`, `addedInIteration`, `children`, `depth`, `failedRapps`, `forwardRuleMatches`, `forwardState`, `id`, `isForcedUnprovable`, `isIrrelevant`, `lastExpandedInIteration`, `mvars`, `normalizationState`, `origin`, `parent`, `preNormGoal`, `state`, `successProbability`, `unsafeQueue`, `unsafeRulesSelected`, `GoalId`, `dummy`, `instDecidableRelLt`, `instHashable`, `instLT`, `instToString`, `one`, `succ`, `toNat`, `zero`, `GoalOrigin`, `originalGoalId?`, `toString`, `GoalRef`, `GoalState`, `instToString`, `isIrrelevant`, `isProven`, `isProvenByNormalization`, `isProvenByRuleApplication`, `isUnknown`, `isUnprovable`, `toEmoji`, `toNodeState`, `GoalUnsafe`, `Iteration`, `instDecidableEq`, `instDecidableRelLe`, `instDecidableRelLt`, `instLE`, `instLT`, `instToString`, `none`, `one`, `succ`, `MVarCluster`, `elim`, `goals`, `isIrrelevant`, `mk`, `modify`, `parent?`, `provenGoal?`, `setGoals`, `setIsIrrelevant`, `setParent`, `setState`, `state`, `MVarClusterData`, `goals`, `isIrrelevant`, `parent?`, `state`, `MVarClusterRef`, `MVarClusterUnsafe`, `NodeState`, `instToString`, `isIrrelevant`, `isProven`, `isUnknown`, `isUnprovable`, `toEmoji`, `NormalizationState`, `isNormal`, `isProvenByNormalization`, `normalizedGoal?`, `Rapp`, `appliedRule`, `assignedMVars`, `children`, `depth`, `elim`, `foldSubgoalsM`, `forSubgoalsM`, `id`, `instBEq`, `instHashable`, `introducedMVars`, `introducesMVar`, `isIrrelevant`, `isSafe`, `metaState`, `mk`, `modify`, `originalSubgoals`, `parent`, `parentPostNormMetaState`, `scriptSteps?`, `setAppliedRule`, `setAssignedMVars`, `setChildren`, `setId`, `setIntroducedMVars`, `setIsIrrelevant`, `setMetaState`, `setOriginalSubgoals`, `setParent`, `setScriptSteps?`, `setState`, `setSuccessProbability`, `state`, `subgoals`, `successProbability`, `RappData`, `appliedRule`, `assignedMVars`, `children`, `id`, `introducedMVars`, `isIrrelevant`, `metaState`, `originalSubgoals`, `parent`, `scriptSteps?`, `state`, `successProbability`, `RappId`, `dummy`, `instDecidableRelLt`, `instHashable`, `instLT`, `instToString`, `one`, `succ`, `toNat`, `zero`, `RappRef`, `getChildAuxDeclNameGenerator`, `RappUnsafe`, `TreeSpec`, `Goal`, `MVarCluster`, `Rapp`, `elimGoal`, `elimMVarCluster`, `elimRapp`, `introGoal`, `introMVarCluster`, `introRapp`, `instBEqGoalState`, `beq`, `instBEqNodeState`, `beq`, `instDecidableEqGoalId`, `decEq`, `instDecidableEqRappId`, `decEq`, `instInhabitedGoalId`, `default`, `instInhabitedGoalOrigin`, `default`, `instInhabitedGoalState`, `default`, `instInhabitedIteration`, `instInhabitedMVarClusterData`, `default`, `instInhabitedNodeState`, `default`, `instInhabitedNormalizationState`, `default`, `instInhabitedRappId`, `default`, `tree`, `treeImpl`	247
Theorems `instNonempty`, `instNonempty`, `instNonempty`, `instNonemptyGoalData`, `instNonemptyRappData`, `instNonemptyTreeSpec`	6
Total	253

Aesop

Definitions

Name	Category	Theorems
`Goal` 📖	CompOp	1 math math: `Goal.instNonempty`
`GoalData` 📖	CompData	1 math math: `instNonemptyGoalData`
`GoalId` 📖	CompData	—
`GoalOrigin` 📖	CompData	—
`GoalRef` 📖	CompOp	—
`GoalState` 📖	CompData	—
`GoalUnsafe` 📖	CompData	—
`Iteration` 📖	CompOp	—
`MVarCluster` 📖	CompOp	1 math math: `MVarCluster.instNonempty`
`MVarClusterData` 📖	CompData	—
`MVarClusterRef` 📖	CompOp	—
`MVarClusterUnsafe` 📖	CompData	—
`NodeState` 📖	CompData	—
`NormalizationState` 📖	CompData	—
`Rapp` 📖	CompOp	1 math math: `Rapp.instNonempty`
`RappData` 📖	CompData	1 math math: `instNonemptyRappData`
`RappId` 📖	CompData	—
`RappRef` 📖	CompOp	—
`RappUnsafe` 📖	CompData	—
`TreeSpec` 📖	CompData	1 math math: `instNonemptyTreeSpec`
`instBEqGoalState` 📖	CompOp	—
`instBEqNodeState` 📖	CompOp	—
`instDecidableEqGoalId` 📖	CompOp	—
`instDecidableEqRappId` 📖	CompOp	—
`instInhabitedGoalId` 📖	CompOp	—
`instInhabitedGoalOrigin` 📖	CompOp	—
`instInhabitedGoalState` 📖	CompOp	—
`instInhabitedIteration` 📖	CompOp	—
`instInhabitedMVarClusterData` 📖	CompOp	—
`instInhabitedNodeState` 📖	CompOp	—
`instInhabitedNormalizationState` 📖	CompOp	—
`instInhabitedRappId` 📖	CompOp	—
`tree` 📖	CompOp	—
`treeImpl` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonemptyGoalData` 📖	mathematical	—	`GoalData`	—	—
`instNonemptyRappData` 📖	mathematical	—	`RappData`	—	—
`instNonemptyTreeSpec` 📖	mathematical	—	`TreeSpec`	—	`instNonemptyGoalData` `instNonemptyRappData`

Aesop.Goal

Definitions

Name	Category	Theorems
`addedInIteration` 📖	CompOp	—
`children` 📖	CompOp	—
`currentGoal` 📖	CompOp	—
`currentGoalAndMetaState` 📖	CompOp	—
`depth` 📖	CompOp	—
`elim` 📖	CompOp	—
`failedRapps` 📖	CompOp	—
`firstProvenRapp?` 📖	CompOp	—
`forwardRuleMatches` 📖	CompOp	—
`forwardState` 📖	CompOp	—
`hasMVar` 📖	CompOp	—
`hasProvableRapp` 📖	CompOp	—
`hasSafeRapp` 📖	CompOp	—
`id` 📖	CompOp	—
`instBEq` 📖	CompOp	—
`instHashable` 📖	CompOp	—
`isActive` 📖	CompOp	—
`isExhausted` 📖	CompOp	—
`isForcedUnprovable` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`isNormal` 📖	CompOp	—
`isRoot` 📖	CompOp	—
`isUnsafeExhausted` 📖	CompOp	—
`lastExpandedInIteration` 📖	CompOp	—
`mk` 📖	CompOp	—
`modify` 📖	CompOp	—
`mvars` 📖	CompOp	—
`normalizationState` 📖	CompOp	—
`origin` 📖	CompOp	—
`originalGoalId` 📖	CompOp	—
`parent` 📖	CompOp	—
`parentMetaState` 📖	CompOp	—
`parentRapp?` 📖	CompOp	—
`postNormGoal?` 📖	CompOp	—
`postNormGoalAndMetaState?` 📖	CompOp	—
`preNormGoal` 📖	CompOp	—
`priority` 📖	CompOp	—
`safeRapps` 📖	CompOp	—
`setAddedInIteration` 📖	CompOp	—
`setChildren` 📖	CompOp	—
`setDepth` 📖	CompOp	—
`setFailedRapps` 📖	CompOp	—
`setForwardRuleMatches` 📖	CompOp	—
`setForwardState` 📖	CompOp	—
`setId` 📖	CompOp	—
`setIsForcedUnprovable` 📖	CompOp	—
`setIsIrrelevant` 📖	CompOp	—
`setLastExpandedInIteration` 📖	CompOp	—
`setMVars` 📖	CompOp	—
`setNormalizationState` 📖	CompOp	—
`setOrigin` 📖	CompOp	—
`setParent` 📖	CompOp	—
`setPreNormGoal` 📖	CompOp	—
`setState` 📖	CompOp	—
`setSuccessProbability` 📖	CompOp	—
`setUnsafeQueue` 📖	CompOp	—
`setUnsafeRulesSelected` 📖	CompOp	—
`state` 📖	CompOp	—
`successProbability` 📖	CompOp	—
`unsafeQueue` 📖	CompOp	—
`unsafeQueue?` 📖	CompOp	—
`unsafeRulesSelected` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonempty` 📖	mathematical	—	`Aesop.Goal`	—	`Aesop.instNonemptyGoalData` `Aesop.MVarCluster.instNonempty`

Aesop.GoalData

Definitions

Name	Category	Theorems
`addedInIteration` 📖	CompOp	—
`children` 📖	CompOp	—
`depth` 📖	CompOp	—
`failedRapps` 📖	CompOp	—
`forwardRuleMatches` 📖	CompOp	—
`forwardState` 📖	CompOp	—
`id` 📖	CompOp	—
`isForcedUnprovable` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`lastExpandedInIteration` 📖	CompOp	—
`mvars` 📖	CompOp	—
`normalizationState` 📖	CompOp	—
`origin` 📖	CompOp	—
`parent` 📖	CompOp	—
`preNormGoal` 📖	CompOp	—
`state` 📖	CompOp	—
`successProbability` 📖	CompOp	—
`unsafeQueue` 📖	CompOp	—
`unsafeRulesSelected` 📖	CompOp	—

Aesop.GoalId

Definitions

Name	Category	Theorems
`dummy` 📖	CompOp	—
`instDecidableRelLt` 📖	CompOp	—
`instHashable` 📖	CompOp	—
`instLT` 📖	CompOp	—
`instToString` 📖	CompOp	—
`one` 📖	CompOp	—
`succ` 📖	CompOp	—
`toNat` 📖	CompOp	—
`zero` 📖	CompOp	—

Aesop.GoalOrigin

Definitions

Name	Category	Theorems
`originalGoalId?` 📖	CompOp	—
`toString` 📖	CompOp	—

Aesop.GoalState

Definitions

Name	Category	Theorems
`instToString` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`isProven` 📖	CompOp	—
`isProvenByNormalization` 📖	CompOp	—
`isProvenByRuleApplication` 📖	CompOp	—
`isUnknown` 📖	CompOp	—
`isUnprovable` 📖	CompOp	—
`toEmoji` 📖	CompOp	—
`toNodeState` 📖	CompOp	—

Aesop.Iteration

Definitions

Name	Category	Theorems
`instDecidableEq` 📖	CompOp	—
`instDecidableRelLe` 📖	CompOp	—
`instDecidableRelLt` 📖	CompOp	—
`instLE` 📖	CompOp	—
`instLT` 📖	CompOp	—
`instToString` 📖	CompOp	—
`none` 📖	CompOp	—
`one` 📖	CompOp	—
`succ` 📖	CompOp	—

Aesop.MVarCluster

Definitions

Name	Category	Theorems
`elim` 📖	CompOp	—
`goals` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`mk` 📖	CompOp	—
`modify` 📖	CompOp	—
`parent?` 📖	CompOp	—
`provenGoal?` 📖	CompOp	—
`setGoals` 📖	CompOp	—
`setIsIrrelevant` 📖	CompOp	—
`setParent` 📖	CompOp	—
`setState` 📖	CompOp	—
`state` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonempty` 📖	mathematical	—	`Aesop.MVarCluster`	—	—

Aesop.MVarClusterData

Definitions

Name	Category	Theorems
`goals` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`parent?` 📖	CompOp	—
`state` 📖	CompOp	—

Aesop.NodeState

Definitions

Name	Category	Theorems
`instToString` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`isProven` 📖	CompOp	—
`isUnknown` 📖	CompOp	—
`isUnprovable` 📖	CompOp	—
`toEmoji` 📖	CompOp	—

Aesop.NormalizationState

Definitions

Name	Category	Theorems
`isNormal` 📖	CompOp	—
`isProvenByNormalization` 📖	CompOp	—
`normalizedGoal?` 📖	CompOp	—

Aesop.Rapp

Definitions

Name	Category	Theorems
`appliedRule` 📖	CompOp	—
`assignedMVars` 📖	CompOp	—
`children` 📖	CompOp	—
`depth` 📖	CompOp	—
`elim` 📖	CompOp	—
`foldSubgoalsM` 📖	CompOp	—
`forSubgoalsM` 📖	CompOp	—
`id` 📖	CompOp	—
`instBEq` 📖	CompOp	—
`instHashable` 📖	CompOp	—
`introducedMVars` 📖	CompOp	—
`introducesMVar` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`isSafe` 📖	CompOp	—
`metaState` 📖	CompOp	—
`mk` 📖	CompOp	—
`modify` 📖	CompOp	—
`originalSubgoals` 📖	CompOp	—
`parent` 📖	CompOp	—
`parentPostNormMetaState` 📖	CompOp	—
`scriptSteps?` 📖	CompOp	—
`setAppliedRule` 📖	CompOp	—
`setAssignedMVars` 📖	CompOp	—
`setChildren` 📖	CompOp	—
`setId` 📖	CompOp	—
`setIntroducedMVars` 📖	CompOp	—
`setIsIrrelevant` 📖	CompOp	—
`setMetaState` 📖	CompOp	—
`setOriginalSubgoals` 📖	CompOp	—
`setParent` 📖	CompOp	—
`setScriptSteps?` 📖	CompOp	—
`setState` 📖	CompOp	—
`setSuccessProbability` 📖	CompOp	—
`state` 📖	CompOp	—
`subgoals` 📖	CompOp	—
`successProbability` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonempty` 📖	mathematical	—	`Aesop.Rapp`	—	`Aesop.instNonemptyRappData` `Aesop.Goal.instNonempty`

Aesop.RappData

Definitions

Name	Category	Theorems
`appliedRule` 📖	CompOp	—
`assignedMVars` 📖	CompOp	—
`children` 📖	CompOp	—
`id` 📖	CompOp	—
`introducedMVars` 📖	CompOp	—
`isIrrelevant` 📖	CompOp	—
`metaState` 📖	CompOp	—
`originalSubgoals` 📖	CompOp	—
`parent` 📖	CompOp	—
`scriptSteps?` 📖	CompOp	—
`state` 📖	CompOp	—
`successProbability` 📖	CompOp	—

Aesop.RappId

Definitions

Name	Category	Theorems
`dummy` 📖	CompOp	—
`instDecidableRelLt` 📖	CompOp	—
`instHashable` 📖	CompOp	—
`instLT` 📖	CompOp	—
`instToString` 📖	CompOp	—
`one` 📖	CompOp	—
`succ` 📖	CompOp	—
`toNat` 📖	CompOp	—
`zero` 📖	CompOp	—

Aesop.RappRef

Definitions

Name	Category	Theorems
`getChildAuxDeclNameGenerator` 📖	CompOp	—

Aesop.TreeSpec

Definitions

Name	Category	Theorems
`Goal` 📖	CompOp	—
`MVarCluster` 📖	CompOp	—
`Rapp` 📖	CompOp	—
`elimGoal` 📖	CompOp	—
`elimMVarCluster` 📖	CompOp	—
`elimRapp` 📖	CompOp	—
`introGoal` 📖	CompOp	—
`introMVarCluster` 📖	CompOp	—
`introRapp` 📖	CompOp	—

Aesop.instBEqGoalState

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Aesop.instBEqNodeState

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Aesop.instDecidableEqGoalId

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Aesop.instDecidableEqRappId

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Aesop.instInhabitedGoalId

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedGoalOrigin

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedGoalState

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedMVarClusterData

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedNodeState

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedNormalizationState

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedRappId

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index