Enum TLExpr 

pub enum TLExpr {
    Pred {
        name: String,
        args: Vec<Term>,
    },
    And(Box<TLExpr>, Box<TLExpr>),
    Or(Box<TLExpr>, Box<TLExpr>),
    Not(Box<TLExpr>),
    Exists {
        var: String,
        domain: String,
        body: Box<TLExpr>,
    },
    ForAll {
        var: String,
        domain: String,
        body: Box<TLExpr>,
    },
    Imply(Box<TLExpr>, Box<TLExpr>),
    Score(Box<TLExpr>),
    Add(Box<TLExpr>, Box<TLExpr>),
    Sub(Box<TLExpr>, Box<TLExpr>),
    Mul(Box<TLExpr>, Box<TLExpr>),
    Div(Box<TLExpr>, Box<TLExpr>),
    Pow(Box<TLExpr>, Box<TLExpr>),
    Mod(Box<TLExpr>, Box<TLExpr>),
    Min(Box<TLExpr>, Box<TLExpr>),
    Max(Box<TLExpr>, Box<TLExpr>),
    Abs(Box<TLExpr>),
    Floor(Box<TLExpr>),
    Ceil(Box<TLExpr>),
    Round(Box<TLExpr>),
    Sqrt(Box<TLExpr>),
    Exp(Box<TLExpr>),
    Log(Box<TLExpr>),
    Sin(Box<TLExpr>),
    Cos(Box<TLExpr>),
    Tan(Box<TLExpr>),
    Eq(Box<TLExpr>, Box<TLExpr>),
    Lt(Box<TLExpr>, Box<TLExpr>),
    Gt(Box<TLExpr>, Box<TLExpr>),
    Lte(Box<TLExpr>, Box<TLExpr>),
    Gte(Box<TLExpr>, Box<TLExpr>),
    IfThenElse {
        condition: Box<TLExpr>,
        then_branch: Box<TLExpr>,
        else_branch: Box<TLExpr>,
    },
    Constant(f64),
    Aggregate {
        op: AggregateOp,
        var: String,
        domain: String,
        body: Box<TLExpr>,
        group_by: Option<Vec<String>>,
    },
    Let {
        var: String,
        value: Box<TLExpr>,
        body: Box<TLExpr>,
    },
    Box(Box<TLExpr>),
    Diamond(Box<TLExpr>),
    Next(Box<TLExpr>),
    Eventually(Box<TLExpr>),
    Always(Box<TLExpr>),
    Until {
        before: Box<TLExpr>,
        after: Box<TLExpr>,
    },
    TNorm {
        kind: TNormKind,
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    TCoNorm {
        kind: TCoNormKind,
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    FuzzyNot {
        kind: FuzzyNegationKind,
        expr: Box<TLExpr>,
    },
    FuzzyImplication {
        kind: FuzzyImplicationKind,
        premise: Box<TLExpr>,
        conclusion: Box<TLExpr>,
    },
    SoftExists {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        temperature: f64,
    },
    SoftForAll {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        temperature: f64,
    },
    WeightedRule {
        weight: f64,
        rule: Box<TLExpr>,
    },
    ProbabilisticChoice {
        alternatives: Vec<(f64, TLExpr)>,
    },
    Release {
        released: Box<TLExpr>,
        releaser: Box<TLExpr>,
    },
    WeakUntil {
        before: Box<TLExpr>,
        after: Box<TLExpr>,
    },
    StrongRelease {
        released: Box<TLExpr>,
        releaser: Box<TLExpr>,
    },
    Lambda {
        var: String,
        var_type: Option<String>,
        body: Box<TLExpr>,
    },
    Apply {
        function: Box<TLExpr>,
        argument: Box<TLExpr>,
    },
    SetMembership {
        element: Box<TLExpr>,
        set: Box<TLExpr>,
    },
    SetUnion {
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    SetIntersection {
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    SetDifference {
        left: Box<TLExpr>,
        right: Box<TLExpr>,
    },
    SetCardinality {
        set: Box<TLExpr>,
    },
    EmptySet,
    SetComprehension {
        var: String,
        domain: String,
        condition: Box<TLExpr>,
    },
    CountingExists {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        min_count: usize,
    },
    CountingForAll {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        min_count: usize,
    },
    ExactCount {
        var: String,
        domain: String,
        body: Box<TLExpr>,
        count: usize,
    },
    Majority {
        var: String,
        domain: String,
        body: Box<TLExpr>,
    },
    LeastFixpoint {
        var: String,
        body: Box<TLExpr>,
    },
    GreatestFixpoint {
        var: String,
        body: Box<TLExpr>,
    },
    Nominal {
        name: String,
    },
    At {
        nominal: String,
        formula: Box<TLExpr>,
    },
    Somewhere {
        formula: Box<TLExpr>,
    },
    Everywhere {
        formula: Box<TLExpr>,
    },
    AllDifferent {
        variables: Vec<String>,
    },
    GlobalCardinality {
        variables: Vec<String>,
        values: Vec<TLExpr>,
        min_occurrences: Vec<usize>,
        max_occurrences: Vec<usize>,
    },
    Abducible {
        name: String,
        cost: f64,
    },
    Explain {
        formula: Box<TLExpr>,
    },
}

Variants

Pred

Fields

name: String

args: Vec<Term>

And(Box<TLExpr>, Box<TLExpr>)

Or(Box<TLExpr>, Box<TLExpr>)

Not(Box<TLExpr>)

Exists

Fields

var: String

domain: String

body: Box<TLExpr>

ForAll

Fields

var: String

domain: String

body: Box<TLExpr>

Imply(Box<TLExpr>, Box<TLExpr>)

Score(Box<TLExpr>)

Add(Box<TLExpr>, Box<TLExpr>)

Sub(Box<TLExpr>, Box<TLExpr>)

Mul(Box<TLExpr>, Box<TLExpr>)

Div(Box<TLExpr>, Box<TLExpr>)

Pow(Box<TLExpr>, Box<TLExpr>)

Mod(Box<TLExpr>, Box<TLExpr>)

Min(Box<TLExpr>, Box<TLExpr>)

Max(Box<TLExpr>, Box<TLExpr>)

Abs(Box<TLExpr>)

Floor(Box<TLExpr>)

Ceil(Box<TLExpr>)

Round(Box<TLExpr>)

Sqrt(Box<TLExpr>)

Exp(Box<TLExpr>)

Log(Box<TLExpr>)

Sin(Box<TLExpr>)

Cos(Box<TLExpr>)

Tan(Box<TLExpr>)

Eq(Box<TLExpr>, Box<TLExpr>)

Lt(Box<TLExpr>, Box<TLExpr>)

Gt(Box<TLExpr>, Box<TLExpr>)

Lte(Box<TLExpr>, Box<TLExpr>)

Gte(Box<TLExpr>, Box<TLExpr>)

IfThenElse

Fields

condition: Box<TLExpr>

then_branch: Box<TLExpr>

else_branch: Box<TLExpr>

Constant(f64)

Aggregate

Fields

op: AggregateOp

var: String

domain: String

body: Box<TLExpr>

group_by: Option<Vec<String>>

Optional group-by variables

Let

Fields

var: String

value: Box<TLExpr>

body: Box<TLExpr>

Box(Box<TLExpr>)

Necessity operator (□, “box”): something is necessarily true In all possible worlds or states, the expression holds

Diamond(Box<TLExpr>)

Possibility operator (◇, “diamond”): something is possibly true In at least one possible world or state, the expression holds Related to Box by: ◇P = ¬□¬P

Next(Box<TLExpr>)

Next operator (X): true in the next state

Eventually(Box<TLExpr>)

Eventually operator (F): true in some future state

Always(Box<TLExpr>)

Always/Globally operator (G): true in all future states

Until

Until operator (U): first expression holds until second becomes true

Fields

before: Box<TLExpr>

after: Box<TLExpr>

TNorm

T-norm (fuzzy AND) with specified semantics

Fields

kind: TNormKind

left: Box<TLExpr>

right: Box<TLExpr>

TCoNorm

T-conorm (fuzzy OR) with specified semantics

Fields

kind: TCoNormKind

left: Box<TLExpr>

right: Box<TLExpr>

FuzzyNot

Fuzzy negation with specified semantics

Fields

kind: FuzzyNegationKind

expr: Box<TLExpr>

FuzzyImplication

Fuzzy implication operator

Fields

kind: FuzzyImplicationKind

premise: Box<TLExpr>

conclusion: Box<TLExpr>

SoftExists

Soft existential quantifier with temperature parameter Temperature controls how “soft” the quantifier is:

• Low temperature (→0): approaches hard max (standard exists)
• High temperature: smoother aggregation (log-sum-exp)

Fields

var: String

domain: String

body: Box<TLExpr>

temperature: f64

Temperature parameter (default: 1.0)

SoftForAll

Soft universal quantifier with temperature parameter Temperature controls how “soft” the quantifier is:

• Low temperature (→0): approaches hard min (standard forall)
• High temperature: smoother aggregation

Fields

var: String

domain: String

body: Box<TLExpr>

temperature: f64

Temperature parameter (default: 1.0)

WeightedRule

Weighted rule with confidence/probability Used in probabilistic logic programming

Fields

weight: f64

rule: Box<TLExpr>

ProbabilisticChoice

Probabilistic choice between alternatives with given probabilities Probabilities should sum to 1.0

Fields

alternatives: Vec<(f64, TLExpr)>

Release

Release operator (R): dual of Until P R Q means Q holds until and including when P becomes true

Fields

released: Box<TLExpr>

releaser: Box<TLExpr>

WeakUntil

Weak Until (W): P W Q means P holds until Q, but Q may never hold

Fields

before: Box<TLExpr>

after: Box<TLExpr>

StrongRelease

Strong Release (M): dual of weak until

Fields

released: Box<TLExpr>

releaser: Box<TLExpr>

Lambda

Lambda abstraction: λvar. body Creates a function that binds var in body

Fields

var: String

var_type: Option<String>

Optional type annotation for the parameter

body: Box<TLExpr>

Apply

Function application: Apply(f, arg) represents f(arg)

Fields

function: Box<TLExpr>

argument: Box<TLExpr>

SetMembership

Set membership: elem ∈ set

Fields

element: Box<TLExpr>

set: Box<TLExpr>

SetUnion

Set union: A ∪ B

Fields

left: Box<TLExpr>

right: Box<TLExpr>

SetIntersection

Set intersection: A ∩ B

Fields

left: Box<TLExpr>

right: Box<TLExpr>

SetDifference

Set difference: A \ B

Fields

left: Box<TLExpr>

right: Box<TLExpr>

SetCardinality

Set cardinality: |S|

Fields

set: Box<TLExpr>

EmptySet

Empty set: ∅

SetComprehension

Set comprehension: { var : domain | condition }

Fields

var: String

domain: String

condition: Box<TLExpr>

CountingExists

Counting existential quantifier: ∃≥k x. P(x) “There exist at least k elements satisfying P”

Fields

var: String

domain: String

body: Box<TLExpr>

min_count: usize

Minimum count threshold

CountingForAll

Counting universal quantifier: ∀≥k x. P(x) “At least k elements satisfy P”

Fields

var: String

domain: String

body: Box<TLExpr>

min_count: usize

Minimum count threshold

ExactCount

Exact count quantifier: ∃=k x. P(x) “Exactly k elements satisfy P”

Fields

var: String

domain: String

body: Box<TLExpr>

count: usize

Exact count required

Majority

Majority quantifier: Majority x. P(x) “More than half of the elements satisfy P”

Fields

var: String

domain: String

body: Box<TLExpr>

LeastFixpoint

Least fixed point (mu): μX. F(X) Used for inductive definitions

Fields

var: String

Variable representing the fixed point

body: Box<TLExpr>

Function body that references var

GreatestFixpoint

Greatest fixed point (nu): νX. F(X) Used for coinductive definitions

Fields

var: String

Variable representing the fixed point

body: Box<TLExpr>

Function body that references var

Nominal

Nominal (named state/world): @i Represents a specific named state in a model

Fields

name: String

At

Satisfaction operator: @i φ “Formula φ is true at the nominal state i”

Fields

nominal: String

formula: Box<TLExpr>

Somewhere

Universal modality: E φ “φ is true in some state reachable from here”

Fields

formula: Box<TLExpr>

Everywhere

Universal modality (dual): A φ “φ is true in all reachable states”

Fields

formula: Box<TLExpr>

AllDifferent

All-different constraint: all variables must have different values

Fields

variables: Vec<String>

GlobalCardinality

Global cardinality constraint Each value in values must occur at least min and at most max times in variables

Fields

variables: Vec<String>

values: Vec<TLExpr>

min_occurrences: Vec<usize>

max_occurrences: Vec<usize>

Abducible

Abducible literal: can be assumed true for explanation

Fields

name: String

cost: f64

Explain

Explanation marker: indicates this part needs explanation

Fields

formula: Box<TLExpr>

Implementations

impl TLExpr

pub fn free_vars(&self) -> HashSet<String>

Collect all free variables in this expression

pub fn all_predicates(&self) -> HashMap<String, usize>

Collect all predicates and their arities

impl TLExpr

pub fn validate_domains(&self, registry: &DomainRegistry) -> Result<(), IrError>

Validate all domain references in this expression.

Checks that:

• All quantifier domains exist in the registry
• Variables used consistently across different quantifiers

pub fn referenced_domains(&self) -> Vec<String>

Extract all domains referenced in this expression.

impl TLExpr

pub fn validate_arity(&self) -> Result<(), String>

Validate that all predicates with the same name have consistent arity

impl TLExpr

pub fn pred(name: impl Into<String>, args: Vec<Term>) -> Self

pub fn and(left: TLExpr, right: TLExpr) -> Self

pub fn or(left: TLExpr, right: TLExpr) -> Self

pub fn negate(expr: TLExpr) -> Self

pub fn exists( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn forall( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn imply(premise: TLExpr, conclusion: TLExpr) -> Self

pub fn score(expr: TLExpr) -> Self

pub fn add(left: TLExpr, right: TLExpr) -> Self

pub fn sub(left: TLExpr, right: TLExpr) -> Self

pub fn mul(left: TLExpr, right: TLExpr) -> Self

pub fn div(left: TLExpr, right: TLExpr) -> Self

pub fn pow(left: TLExpr, right: TLExpr) -> Self

pub fn modulo(left: TLExpr, right: TLExpr) -> Self

pub fn min(left: TLExpr, right: TLExpr) -> Self

pub fn max(left: TLExpr, right: TLExpr) -> Self

pub fn abs(expr: TLExpr) -> Self

pub fn floor(expr: TLExpr) -> Self

pub fn ceil(expr: TLExpr) -> Self

pub fn round(expr: TLExpr) -> Self

pub fn sqrt(expr: TLExpr) -> Self

pub fn exp(expr: TLExpr) -> Self

pub fn log(expr: TLExpr) -> Self

pub fn sin(expr: TLExpr) -> Self

pub fn cos(expr: TLExpr) -> Self

pub fn tan(expr: TLExpr) -> Self

pub fn eq(left: TLExpr, right: TLExpr) -> Self

pub fn lt(left: TLExpr, right: TLExpr) -> Self

pub fn gt(left: TLExpr, right: TLExpr) -> Self

pub fn lte(left: TLExpr, right: TLExpr) -> Self

pub fn gte(left: TLExpr, right: TLExpr) -> Self

pub fn if_then_else( condition: TLExpr, then_branch: TLExpr, else_branch: TLExpr, ) -> Self

pub fn constant(value: f64) -> Self

pub fn aggregate( op: AggregateOp, var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn aggregate_with_group_by( op: AggregateOp, var: impl Into<String>, domain: impl Into<String>, body: TLExpr, group_by: Vec<String>, ) -> Self

pub fn count( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn sum( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn average( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn max_agg( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn min_agg( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn product( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

pub fn let_binding(var: impl Into<String>, value: TLExpr, body: TLExpr) -> Self

pub fn modal_box(expr: TLExpr) -> Self

Create a Box (necessity) operator.

□P: “P is necessarily true” - holds in all possible worlds/states

pub fn modal_diamond(expr: TLExpr) -> Self

Create a Diamond (possibility) operator.

◇P: “P is possibly true” - holds in at least one possible world/state

pub fn next(expr: TLExpr) -> Self

Create a Next operator.

XP: “P is true in the next state”

pub fn eventually(expr: TLExpr) -> Self

Create an Eventually operator.

FP: “P will eventually be true” - true in some future state

pub fn always(expr: TLExpr) -> Self

Create an Always operator.

GP: “P is always true” - true in all future states

pub fn until(before: TLExpr, after: TLExpr) -> Self

Create an Until operator.

P U Q: “P holds until Q becomes true”

pub fn tnorm(kind: TNormKind, left: TLExpr, right: TLExpr) -> Self

Create a T-norm (fuzzy AND) operation with specified semantics.

pub fn fuzzy_and(left: TLExpr, right: TLExpr) -> Self

Create a minimum T-norm (standard fuzzy AND).

pub fn probabilistic_and(left: TLExpr, right: TLExpr) -> Self

Create a product T-norm (probabilistic AND).

pub fn tconorm(kind: TCoNormKind, left: TLExpr, right: TLExpr) -> Self

Create a T-conorm (fuzzy OR) operation with specified semantics.

pub fn fuzzy_or(left: TLExpr, right: TLExpr) -> Self

Create a maximum T-conorm (standard fuzzy OR).

pub fn probabilistic_or(left: TLExpr, right: TLExpr) -> Self

Create a probabilistic sum T-conorm.

pub fn fuzzy_not(kind: FuzzyNegationKind, expr: TLExpr) -> Self

Create a fuzzy negation with specified semantics.

pub fn standard_fuzzy_not(expr: TLExpr) -> Self

Create a standard fuzzy negation (1 - x).

pub fn fuzzy_imply( kind: FuzzyImplicationKind, premise: TLExpr, conclusion: TLExpr, ) -> Self

Create a fuzzy implication with specified semantics.

pub fn soft_exists( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, temperature: f64, ) -> Self

Create a soft existential quantifier with temperature parameter.

Arguments

• var - Variable name
• domain - Domain name
• body - Expression body
• temperature - Temperature parameter (default 1.0). Lower = harder max.

pub fn soft_forall( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, temperature: f64, ) -> Self

Create a soft universal quantifier with temperature parameter.

Arguments

• var - Variable name
• domain - Domain name
• body - Expression body
• temperature - Temperature parameter (default 1.0). Lower = harder min.

pub fn weighted_rule(weight: f64, rule: TLExpr) -> Self

Create a weighted rule with confidence/probability.

Arguments

• weight - Weight/confidence (typically in [0,1] for probabilities)
• rule - The rule expression

pub fn probabilistic_choice(alternatives: Vec<(f64, TLExpr)>) -> Self

Create a probabilistic choice between alternatives.

Arguments

• alternatives - Vector of (probability, expression) pairs. Should sum to 1.0.

pub fn release(released: TLExpr, releaser: TLExpr) -> Self

Create a Release operator (R).

P R Q: “Q holds until and including when P becomes true”

pub fn weak_until(before: TLExpr, after: TLExpr) -> Self

Create a Weak Until operator (W).

P W Q: “P holds until Q, but Q may never hold”

pub fn strong_release(released: TLExpr, releaser: TLExpr) -> Self

Create a Strong Release operator (M).

P M Q: Dual of weak until

pub fn lambda( var: impl Into<String>, var_type: Option<String>, body: TLExpr, ) -> Self

Create a lambda abstraction: λvar. body

Arguments

• var - The parameter name
• var_type - Optional type annotation for the parameter
• body - The function body

pub fn lambda_untyped(var: impl Into<String>, body: TLExpr) -> Self

Create a lambda abstraction without type annotation.

pub fn apply(function: TLExpr, argument: TLExpr) -> Self

Create a function application: f(arg)

Arguments

• function - The function to apply
• argument - The argument to apply to the function

pub fn set_membership(element: TLExpr, set: TLExpr) -> Self

Create a set membership test: elem ∈ set

pub fn set_union(left: TLExpr, right: TLExpr) -> Self

Create a set union: A ∪ B

pub fn set_intersection(left: TLExpr, right: TLExpr) -> Self

Create a set intersection: A ∩ B

pub fn set_difference(left: TLExpr, right: TLExpr) -> Self

Create a set difference: A \ B

pub fn set_cardinality(set: TLExpr) -> Self

Create a set cardinality expression: |S|

pub fn empty_set() -> Self

Create an empty set: ∅

pub fn set_comprehension( var: impl Into<String>, domain: impl Into<String>, condition: TLExpr, ) -> Self

Create a set comprehension: { var : domain | condition }

pub fn counting_exists( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, min_count: usize, ) -> Self

Create a counting existential quantifier: ∃≥k x. P(x)

“There exist at least k elements satisfying P”

pub fn counting_forall( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, min_count: usize, ) -> Self

Create a counting universal quantifier: ∀≥k x. P(x)

“At least k elements satisfy P”

pub fn exact_count( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, count: usize, ) -> Self

Create an exact count quantifier: ∃=k x. P(x)

“Exactly k elements satisfy P”

pub fn majority( var: impl Into<String>, domain: impl Into<String>, body: TLExpr, ) -> Self

Create a majority quantifier: Majority x. P(x)

“More than half of the elements satisfy P”

pub fn least_fixpoint(var: impl Into<String>, body: TLExpr) -> Self

Create a least fixed point: μX. F(X)

Used for inductive definitions (smallest solution)

pub fn greatest_fixpoint(var: impl Into<String>, body: TLExpr) -> Self

Create a greatest fixed point: νX. F(X)

Used for coinductive definitions (largest solution)

pub fn nominal(name: impl Into<String>) -> Self

Create a nominal (named state): @i

pub fn at(nominal: impl Into<String>, formula: TLExpr) -> Self

Create a satisfaction operator: @i φ

“Formula φ is true at the nominal state i”

pub fn somewhere(formula: TLExpr) -> Self

Create a “somewhere” modality: E φ

“φ is true in some reachable state”

pub fn everywhere(formula: TLExpr) -> Self

Create an “everywhere” modality: A φ

“φ is true in all reachable states”

pub fn all_different(variables: Vec<String>) -> Self

Create an all-different constraint.

All variables must have different values.

pub fn global_cardinality( variables: Vec<String>, values: Vec<TLExpr>, min_occurrences: Vec<usize>, max_occurrences: Vec<usize>, ) -> Self

Create a global cardinality constraint.

Each value must occur within specified bounds in the variables.

pub fn abducible(name: impl Into<String>, cost: f64) -> Self

Create an abducible literal.

Can be assumed true for explanation with the given cost.

pub fn explain(formula: TLExpr) -> Self

Mark a formula as needing explanation.

pub fn substitute(&self, var: &str, value: &TLExpr) -> Self

Substitute a variable with an expression throughout this formula.

This performs capture-avoiding substitution, respecting variable shadowing in quantifiers, lambda abstractions, and let bindings.

Arguments

• var - The variable name to replace
• value - The expression to substitute in place of the variable

Example

use tensorlogic_ir::{TLExpr, Term};

// P(x) ∧ Q(x)
let p = TLExpr::pred("P", vec![Term::var("x")]);
let q = TLExpr::pred("Q", vec![Term::var("x")]);
let expr = TLExpr::and(p.clone(), q);

// Substitute x with y
let y = TLExpr::pred("y", vec![]);
let result = expr.substitute("x", &y);

Trait Implementations

impl Clone for TLExpr

fn clone(&self) -> TLExpr

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TLExpr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for TLExpr

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for TLExpr

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for TLExpr

fn eq(&self, other: &TLExpr) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for TLExpr

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for TLExpr