Match
📁 Source: Batteries/Data/Array/Match.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsIterator, inner, state, instIteratorIteratorOfMonad, modifyStep, next?, ofArray, ofStream, state, table, PrefixTable, extend, size, step, toArray, instInhabitedPrefixTable, mkPrefixTable, mkPrefixTableOfStream, loop | 19 |
| 2 | |
| Total | 21 |
Array
Definitions
| Name | Category | Theorems |
|---|---|---|
PrefixTable 📖 | CompData | — |
instInhabitedPrefixTable 📖 | CompOp | — |
mkPrefixTable 📖 | CompOp | — |
mkPrefixTableOfStream 📖 | CompOp | — |
Array.Matcher
Definitions
| Name | Category | Theorems |
|---|---|---|
Iterator 📖 | CompData | |
instIteratorIteratorOfMonad 📖 | CompOp | |
modifyStep 📖 | CompOp | — |
next? 📖 | CompOp | — |
ofArray 📖 | CompOp | — |
ofStream 📖 | CompOp | — |
state 📖 | CompOp | — |
table 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
instFiniteIterator 📖 | mathematical | — | IteratorinstIteratorIteratorOfMonad | — | — |
Array.Matcher.Iterator
Definitions
| Name | Category | Theorems |
|---|---|---|
inner 📖 | CompOp | — |
state 📖 | CompOp | — |
Array.PrefixTable
Definitions
| Name | Category | Theorems |
|---|---|---|
extend 📖 | CompOp | — |
size 📖 | CompOp | — |
step 📖 | CompOp | — |
toArray 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
valid 📖 | — | toArray | — | — | — |
Array.mkPrefixTableOfStream
Definitions
| Name | Category | Theorems |
|---|---|---|
loop 📖 | CompOp | — |
---