pub trait TermVisitor<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> {
type T;
type E;
fn visit_constant(&mut self, constant: Constant) -> Result<Self::T, Self::E>;
fn visit_qual_identifier(
&mut self,
qual_identifier: QualIdentifier
) -> Result<Self::T, Self::E>;
fn visit_application(
&mut self,
qual_identifier: QualIdentifier,
arguments: Vec<Self::T>
) -> Result<Self::T, Self::E>;
fn visit_let(
&mut self,
var_bindings: Vec<(Symbol, Self::T)>,
term: Self::T
) -> Result<Self::T, Self::E>;
fn visit_forall(
&mut self,
vars: Vec<(Symbol, Sort)>,
term: Self::T
) -> Result<Self::T, Self::E>;
fn visit_exists(
&mut self,
vars: Vec<(Symbol, Sort)>,
term: Self::T
) -> Result<Self::T, Self::E>;
fn visit_match(
&mut self,
term: Self::T,
cases: Vec<(Vec<Symbol>, Self::T)>
) -> Result<Self::T, Self::E>;
fn visit_attributes(
&mut self,
term: Self::T,
attributes: Vec<(Keyword, AttributeValue<Constant, Symbol, SExpr>)>
) -> Result<Self::T, Self::E>;
}
impl<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> TermVisitor<Constant, QualIdentifier, Keyword, SExpr, Symbol, Sort> for SyntaxBuilder