Crate lsts

Source
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