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