Module formatter

Module formatter 

Source
Expand description

Output formatters for logical expressions.

This module defines the LogicFormatter trait and its implementations for rendering logical expressions in different notations:

  • Unicode: Standard FOL symbols (∀, ∃, ∧, ∨, ¬, →)
  • LaTeX: TeX math mode notation (\forall, \exists, \land, etc.)
  • ASCII: Plain text fallback (ALL, EXISTS, AND, OR, NOT)

Formatters handle quantifiers, connectives, modal operators, temporal operators, and special constructs like plurals and possessives.

Structs§

KripkeFormatter
Formatter for Kripke lowered output with explicit world arguments. Modals are already lowered to quantifiers; this formatter just renders the result with world arguments appended to predicates.
LatexFormatter
RustFormatter
Formatter that produces Rust boolean expressions for runtime assertions. Used by codegen to convert LogicExpr into debug_assert!() compatible code.
SimpleFOLFormatter
UnicodeFormatter

Traits§

LogicFormatter
Trait for formatting logical expressions in various notations.