pub enum Sentence {
Simple(Proposition),
Connected((SentenceConnective, u32, u32)),
Prenex((Vec<String>, u32)),
Quantified((BlockQuant, String, PredicateId, Option<u32>, u32)),
}Expand description
A sentence: a simple proposition, two connected sentences, a prenex-quantified body, or a quantified binder block.
Variants§
Simple(Proposition)
Simple predication.
Connected((SentenceConnective, u32, u32))
Connected sentences. Fields: (connective, left-sentence-id, right-sentence-id).
Prenex((Vec<String>, u32))
Prenex all $x, $y: <body>: a sequence of universally quantified
logic variables scoping a body sentence. Fields: (variable names in
prenex order, body-sentence-id). Lowers to nested ∀ over the body
in nibli-semantics.
Quantified((BlockQuant, String, PredicateId, Option<u32>, u32))
Quantified binder block: exactly N [the] X $v: body / every the X $v: body. Fields: (kind, variable particle $v,
restrictor-predicate-id, optional where-clause-sentence-id folded on
the DOMAIN side, body-sentence-id). The variable binds by name across
the whole block (the prenex mechanism); lowers to Count{v, N, And(domain, body)} / ForAll(v, Or(Not(domain), body)) in
nibli-semantics, where the definite kinds’ domain is the opaque
the_domain_<head> restrictor. (the X $v: blocks never reach the
AST — they desugar by substitution at emission.)