Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- Annotation
Table - A key-value annotation table for arbitrary metadata.
- Axiom
Val - Axiom declaration value.
- Before
After - A pair of values useful for before/after comparisons.
- BiMap
- A bidirectional map between two types.
- Constant
Summary - A summary of a declaration’s key properties.
- Constant
Val - Base constant value shared by all declaration types.
- Constructor
Val - Constructor declaration value.
- Decl
Dependencies - Tracks the dependency graph between declarations.
- Decl
Filter - Filters declarations by kind, namespace, or attributes.
- Decl
Index - An index that maps declaration names to their positions.
- Decl
Signature - The type signature of a declaration (name + type, no body).
- Definition
Val - Definition declaration value.
- Diag
Meta - A key-value store for diagnostic metadata.
- Event
Counter - A simple event counter with named events.
- Frequency
Table - Tracks the frequency of items.
- Generation
- A generation counter for validity tracking.
- IdDispenser
- A counter that dispenses monotonically increasing
TypedIdvalues. - Inductive
Val - Inductive type declaration value.
- Interval
Set - A set of non-overlapping integer intervals.
- Loop
Clock - A clock that measures elapsed time in a loop.
- Memo
Slot - A memoized computation slot that stores a cached value.
- Opaque
Val - Opaque declaration value.
- QuotVal
- Quotient declaration value.
- Recursor
Rule - A single recursor reduction rule.
- Recursor
Val - Recursor (eliminator) declaration value.
- Ring
Buffer - A growable ring buffer with fixed maximum capacity.
- Scope
Stack - A simple stack-based scope tracker.
- SeqNum
- A sequence number that can be compared for ordering.
- Simple
LruCache - A simple LRU cache backed by a linked list + hash map.
- Slot
- A slot that can hold a value, with lazy initialization.
- Sparse
BitSet - A simple sparse bit set.
- Stat
Cache - A counted-access cache that tracks hit and miss statistics.
- String
Interner - Interns strings to save memory (each unique string stored once).
- Theorem
Val - Theorem declaration value.
- Timestamp
- A monotonic timestamp in microseconds.
- TypedId
- A type-safe wrapper around a
u32identifier. - Work
Queue - A FIFO work queue.
- Work
Stack - A simple LIFO work queue.
Enums§
- Constant
Info - Unified constant info enum (mirrors LEAN 4’s
constant_info). - Constant
Kind - The kind of constant declaration.
- Decl
Attr - An attribute that can be attached to a declaration.
- Decl
Kind - The kind of a declaration.
- Decl
Visibility - Visibility of a declaration.
- Definition
Safety - Safety classification for definitions.
- Quot
Kind - Which quotient component a declaration represents.