Packages

implicit class RichTerm[U <: Term with Subs[U]] extends AnyRef

Operations on terms

Linear Supertypes
AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. RichTerm
  2. AnyRef
  3. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new RichTerm(term: U)

Value Members

  1. def :->[V <: Term with Subs[V]](that: V): Func[U, V]

    constructor for (pure) lambda functions, see lmbda

  2. def :~>[V <: Term with Subs[V]](that: V): FuncLike[U, V]

    constructor for (in general dependent) lambda functions, see lambda

  3. def =:=(rhs: U): IdentityTyp[U]

    equality type 'term = rhs'

  4. def refl: Refl[U]

    reflexivity term refl : term = term