public final class LambdaFormula extends QuantifiedTerm
precedence
Modifier and Type | Method and Description |
---|---|
void |
accept(ASTVisitor visitor)
Accept visitor for a visit.
|
static LambdaFormula |
construct(TypedIdentifier[] vars,
Formula body)
Construct a function expression with a formula body.
|
Formula |
getBody()
Get the body of the term.
|
java.lang.String |
getQuantifier()
Get string representation of quantifier.
|
getPrecedence, getType, setType
accept, acceptChildren, getVariables
getPosition, isLeftAssociative, isRightAssociative, setPosition
accept, accept, print, printCore, toString, toStringCore
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
isLeftAssociative, isRightAssociative
getPosition, setPosition
accept, acceptChildren, print, printCore, toString, toStringCore
public static LambdaFormula construct(TypedIdentifier[] vars, Formula body)
vars
- the bound variables of the term.body
- the body of the term.public Formula getBody()
getBody
in class QuantifiedExpression
public java.lang.String getQuantifier()
getQuantifier
in class QuantifiedExpression
public void accept(ASTVisitor visitor)
accept
in interface AST
accept
in class QuantifiedTerm
visitor
- the visitor who is accepted by this node.