Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- Alpha
Equivalence Checker - Check α-equivalence of two terms (de Bruijn terms are equal up to renaming of bound variables by definition — so alpha-equivalence is just structural equality after normalization of bound variable names, which in de Bruijn form is plain equality).
- Beta
Reducer - A β-reducer with configurable strategy and step budget.
- Context
- A typing context: list of types for de Bruijn variables. Index 0 = innermost binder.
- Linear
Type Checker - A simple linearity checker that tracks variable usage counts. In linear typing, each variable must be used exactly once.
- Session
Type Compatibility - Checks compatibility (duality) between two session types.
- Type
Inference System - A bidirectional type inference system for STLC. Implements the “Check” and “Synth” modes of bidirectional typing.
Enums§
- Binary
Session - A session type in the binary session type system.
- Simple
Type - A simple type: base or arrow.
- Strategy
- Strategy for β-reduction.
- Term
- An untyped lambda calculus term using de Bruijn indices.