tla_syntax/lib.rs
1//! Lexer, parser and AST for the fragment of TLA+ that specifications are
2//! written in: modules, declarations, definitions and expressions.
3//!
4//! Temporal formulas are parsed into the AST but carry no meaning here — the
5//! evaluator that consumes this crate answers questions about concrete states,
6//! not about behaviours.
7
8pub mod ast;
9pub mod error;
10mod lexer;
11mod parser;
12mod print;
13pub mod token;
14
15pub use ast::{Bound, Decl, Def, ExceptPath, Expr, LetInstance, Module, Param, QuantKind, Unit};
16pub use error::{Error, Result, Stage};
17pub use lexer::lex;
18pub use parser::{
19 DEFAULT_NESTING_LIMIT, parse_expression, parse_expression_bounded, parse_module,
20 parse_module_bounded,
21};