fmrisc.ProofNavigator.Syntax

Class LambdaTerm

java.lang.Object

fmrisc.ProofNavigator.Syntax.ASTBase

fmrisc.ProofNavigator.Syntax.ExpressionBase

fmrisc.ProofNavigator.Syntax.QuantifiedExpression

fmrisc.ProofNavigator.Syntax.LambdaTerm

All Implemented Interfaces:

AST, Expression

public final class LambdaTerm
extends QuantifiedExpression

Handling of lambda terms.

Constructor Summary

Constructors

Constructor and Description
LambdaTerm(TypedIdentifier[] variables, Expression base) construct lambda term of variables and base term

Method Summary

Modifier and Type	Method and Description
QuantifiedExpression	construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.

Methods inherited from class fmrisc.ProofNavigator.Syntax.QuantifiedExpression

accept, getBase, getPriority, getVariables, instantiate, printCore, substitution

Methods inherited from class fmrisc.ProofNavigator.Syntax.ExpressionBase

printPriority

Methods inherited from class fmrisc.ProofNavigator.Syntax.ASTBase

print, printParens, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface fmrisc.ProofNavigator.Syntax.AST

print, printParens, toString

Constructor Detail

LambdaTerm

public LambdaTerm(TypedIdentifier[] variables,
                  Expression base)

construct lambda term of variables and base term

Parameters:

variables - the quantified variables

base - the base term

Method Detail

construct

public QuantifiedExpression construct(TypedIdentifier[] variables,
                                      Expression base)

Construct quantified expression.

Specified by:

construct in class QuantifiedExpression

Parameters:

variables - typed variables.

base - an expression.

Returns:

a quantified expression of the same kind as this expression with the denoted variables and base expression.