Expand description
Large Scale Type Systems: LSTS implements a categorical view of typed lambda calculus with flexible soundness guarantees.
Modulesยง
- constant
- The Constant module provides value constants for dynamic evaluation in dependent types
- debug
- The Debug module defines error messages and formatting
- dfa
- The DFA module defines Deterministic Finite Automata and operations on them
- kind
- The Kind module provides abstractions over Kinds. A Term has at least the kind Term. A Type has precisely one Kind unless that Type is an And. A Kind can always be written as K1<K2,K3> for Kinds K1, K2, and K3. There are three intrinsic Kinds: Nil, Term, and Constant.
- ll
- The LL module defines an LL(1) hand written parser.
- scope
- The Scope module defines the shape of a typing and evaluation context.
- term
- The Term module defines lambda calculus expressions.
- tlc
- The TLC module provides a context object for parsing, typing, and evaluating expressions.
- token
- The Token module defines lexical tokens, spans, and a stream tokenizer
- typ
- The Typ module provides abstractions over Types.
- util
- General quality-of-life services in Rust