Skip to content

Every Tenor contract uses these symbols in predicates, transitions, and quantifiers. The parser accepts both Unicode and ASCII forms. Unicode is conventional in docs and examples. ASCII works everywhere.

Logical Operators

SymbolASCIINameMeaningExample
andConjunctionBoth sides must be truepayment_ok = true ∧ dispute_filed = false
orDisjunctionEither side can be truestatus = "cancelled" ∨ status = "expired"
¬notNegationInverts the condition¬ verdict_present(override_approved)

Quantifiers

SymbolASCIINameMeaningExample
forallUniversalTrue for every element in a list∀ item in line_items . item.amount > 0
existsExistentialTrue for at least one element∃ doc in documents . doc.status = "verified"

Quantifiers bind over List-typed facts or List-typed Record fields. The . after the list reference introduces the body predicate — it is NOT the field access operator in this position.

Comparison Operators

SymbolASCIIMeaningApplies to
==EqualAll types
!=Not equalAll types
<<Less thanInt, Decimal, Money, Date, DateTime
<=Less or equalInt, Decimal, Money, Date, DateTime
>>Greater thanInt, Decimal, Money, Date, DateTime
>=Greater or equalInt, Decimal, Money, Date, DateTime

Not available on: Bool (only = ), Text (only = ), Enum (only = ). Attempting < on a Bool is an elaboration error.

Money comparison: both sides must be the same currency. Money(USD) < Money(EUR) is a type error.

Arithmetic Operators

SymbolMeaningRestrictionExample
+AdditionInt, Decimal, Moneybase_amount + surcharge
-SubtractionInt, Decimal, Money; also DateTime - DateTime → Durationtotal - discount
*MultiplicationLiteral onlyfact * 3 is allowed, fact1 * fact2 is forbiddenunit_price * 100

The multiplication restriction is deliberate. Variable × variable would require unbounded range analysis. Literal multiplication keeps ranges statically checkable.

Field Access

SymbolNameMeaningExample
.DotAccess a field on a Record-typed factplan_features.max_seats

When a fact has type Record(fields), the . operator accesses a named field. Chaining is supported for nested records: order.billing_address.zip_code.

Inside quantifiers: The . after ∀ item in list introduces the body predicate — this is syntactically distinct from field access. ∀ item in line_items . item.amount > 0 has two dots: the first separates the binding from the body, the second accesses the amount field on item.

Transition Arrow

SymbolASCIIMeaningExample
->State transition(EscrowAccount, held, released) in effects; (held, released) in entity transitions

Used in entity transition declarations and operation effects. Both forms are identical to the parser.

Special Functions

FunctionMeaningExample
verdict_present(id)True if the named verdict was produced by rule evaluationverdict_present(payment_verified)
len(list)Length of a List-typed value (operator on ground term, not a built-in function)len(line_items) > 0

verdict_present is the bridge between strata — a stratum 1 rule checks whether stratum 0 produced a verdict.

There are no other built-in functions. No now(), no abs(), no sqrt(), no string functions. All time-varying values enter as Facts.

Precedence

From highest to lowest:

  1. . (field access)
  2. ¬ / not
  3. * (multiplication)
  4. +, -
  5. =, , <, , >,
  6. / and
  7. / or
  8. , (quantifiers bind loosest)

Parentheses override precedence as expected.