Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- Builtin
Prec Table - A precedence table for built-in operators.
- Macro
Rule - A macro rule with parameters.
- Notation
Conflict - A notation conflict: two rules with the same pattern but different expansions.
- Notation
Entry - A registered notation declaration.
- Notation
Env - A notation environment with scoped rules.
- Notation
Formatter - A simple notation formatter that expands
_ op _patterns. - Notation
Group - A notation group that bundles related notation rules.
- Notation
Priority Queue - A priority queue for notation rules (by precedence).
- Notation
Registry - A simple notation registry that maps patterns to rules.
- Notation
Rule - A user-defined notation rule.
- Notation
Scope - A notation scope for open/close semantics.
- Notation
Table - The main notation/operator table.
- Operator
Alias - An operator alias entry.
- Operator
Alias Table - A collection of operator aliases.
- Operator
Entry - A registered operator (simpler than a full notation entry).
- Overload
Entry - An overloaded operator entry.
- Overload
Registry - A registry of operator overloads.
- Pattern
Matcher - A simple token pattern matcher for notation expansion.
- Prec
Level - A notation precedence level with associativity.
- Scope
Guard - A scope guard that automatically pops when dropped.
- Syntax
Extension - A syntax extension hook.
- Syntax
Sugar - An abstract syntax sugar definition.
- Syntax
Sugar Library - A collection of syntax sugar definitions.
Enums§
- Fixity
- Fixity of an operator entry.
- Notation
Category - A notation category (e.g. term, tactic, command).
- Notation
Kind - The kind of a notation declaration.
- Notation
Part - A single part of a notation pattern.
- Notation
Token Kind - A notation token kind for pattern matching.