Documentation Verification Report

UScriptToSScript

📁 Source: Aesop/Script/UScriptToSScript.lean

Statistics

Metric	Count
Definitions `StepTree`, `focusableGoals`, `numSiblings`, `toMessageData`, `toMessageData?`, `toStepTree`, `instToMessageDataStepTree`, `isConsecutiveSequence`, `orderedUScriptToSScript`, `sortDedupArrays`	10
Theorems `instNonemptyStepTree`	1
Total	11

Aesop.Script

Definitions

Name	Category	Theorems
`StepTree` 📖	CompData	1 math math: `instNonemptyStepTree`
`instToMessageDataStepTree` 📖	CompOp	—
`isConsecutiveSequence` 📖	CompOp	—
`orderedUScriptToSScript` 📖	CompOp	—
`sortDedupArrays` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonemptyStepTree` 📖	mathematical	—	`StepTree`	—	—

Aesop.Script.StepTree

Definitions

Name	Category	Theorems
`focusableGoals` 📖	CompOp	—
`numSiblings` 📖	CompOp	—
`toMessageData` 📖	CompOp	—
`toMessageData?` 📖	CompOp	—

Aesop.Script.UScript

Definitions

Name	Category	Theorems
`toStepTree` 📖	CompOp	—

---

← Back to Index