Type Members

1.  trait ExprSubstWithβ0 extends AnyRef
2.  trait ExprSubstWithβ1 extends ExprSubstWithβ0
3.  trait ExprSubstitutable1 extends AnyRef
4.  trait ExprSubstitutable2 extends ExprSubstitutable1
5.  trait ExprSubstitutable3 extends ExprSubstitutable2
6.  trait ExprSubstitutable4 extends ExprSubstitutable3
7.  trait ExprSubstitutable5 extends ExprSubstitutable4
8.  trait ExprSubstitutable6 extends ExprSubstitutable5
9.  trait ExprSubstitutable7 extends ExprSubstitutable6
10.  class FOLSubstitution extends Substitution
11.  class PreSubstitution extends AnyRef

    An unvalidated substitution, you should use Substitution instead.

12.  trait SeqSubstitutable extends AnyRef
13.  trait Substitutable[-S <: Substitution, -T, +U] extends AnyRef

    Trait that describes the following relation between types S, T, U: If a substitution of type S is applied to an element of type T, the result will have type U.

    Trait that describes the following relation between types S, T, U: If a substitution of type S is applied to an element of type T, the result will have type U.

    S

    A subtype of Substitution.

    T

    The input type.

    U

    The output type.

    Annotations

    @implicitNotFound()

14.  class Substitution extends PreSubstitution

    A substitution is a mapping from variables to lambda-expressions which differs from the identity on finitely many variables.

    A substitution is a mapping from variables to lambda-expressions which differs from the identity on finitely many variables. Therefore: 1) each variable is mapped to only one lambda expression 2) the order of the variable-mappings is irrelevant 3) all variable-mappings are applied simultaneously to a term i.e. {x |-> y, y |-> a}x = y and not a.

    As the lambda calculus contains variable binders, substitution can only be defined up to alpha-equivalence. When applying a substitution, bound variables are renamed if needed.