| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Conformance.Lean.Registration
Description
Bind the registration theorem to the shared model comparison.
Synopsis
- data InsertActive
- modelComparison :: LeanCheck (LiveI reg wal step obs cmp) InsertActive step
- insertActiveRow :: Theorem InsertActive
Documentation
data InsertActive Source #
The registration declaration, distinct from every other theorem marker.
modelComparison :: LeanCheck (LiveI reg wal step obs cmp) InsertActive step Source #