Tracing
📁 Source: Aesop/Tracing.lean
Statistics
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
TraceOption 📖 | CompData | — |
exceptRuleResultToEmoji 📖 | CompOp | — |
instInhabitedTraceOption 📖 | CompOp | — |
newNodeEmoji 📖 | CompOp | — |
nodeProvedEmoji 📖 | CompOp | — |
nodeUnknownEmoji 📖 | CompOp | — |
nodeUnprovableEmoji 📖 | CompOp | — |
registerTraceOption 📖 | CompOp | — |
resolveTraceOption 📖 | CompOp | — |
ruleErrorEmoji 📖 | CompOp | — |
ruleFailureEmoji 📖 | CompOp | — |
rulePostponedEmoji 📖 | CompOp | — |
ruleProvedEmoji 📖 | CompOp | — |
ruleSkippedEmoji 📖 | CompOp | — |
ruleSuccessEmoji 📖 | CompOp | — |
traceSimpTheoremTreeContents 📖 | CompOp | — |
traceSimpTheorems 📖 | CompOp | — |
withAesopTraceNode 📖 | CompOp | — |
withAesopTraceNodeBefore 📖 | CompOp | — |
withConstAesopTraceNode 📖 | CompOp | — |
«doElemAesop_trace![_]__» 📖 | CompOp | — |
«doElemAesop_trace[_]___» 📖 | CompOp | — |
Aesop.TraceOption
Definitions
| Name | Category | Theorems |
|---|---|---|
debug 📖 | CompOp | — |
extraction 📖 | CompOp | — |
forward 📖 | CompOp | — |
forwardDebug 📖 | CompOp | — |
isEnabled 📖 | CompOp | — |
option 📖 | CompOp | — |
proof 📖 | CompOp | — |
rpinf 📖 | CompOp | — |
ruleSet 📖 | CompOp | — |
script 📖 | CompOp | — |
stats 📖 | CompOp | — |
steps 📖 | CompOp | — |
traceClass 📖 | CompOp | — |
tree 📖 | CompOp | — |
withEnabled 📖 | CompOp | — |
Aesop.instInhabitedTraceOption
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---