Packages

trait Subs[+U <: Term] extends AnyRef

specify result of substitution a typical class is closed under substitution.

Self Type
U with Subs[U] with Term
Linear Supertypes
AnyRef, Any
Known Subclasses
AbsPair, AtomicTerm, Cnst, CnstFunc, CnstFuncLike, Composition, ConstantTerm, ConstantTyp, DepFunc, DepFuncDefn, DepPair, DepSymbolicFunc, Equality, Func, FuncDefn, FuncLike, FuncTyp, GenFuncTyp, IdentityTyp, InducFn, RecFn, IndInducFuncLike, IndRecFunc, InducFuncLike, LambdaFixed, LambdaLike, LambdaTerm, MiscAppln, NamedDepFunc, NamedFunc, OptDepFuncDefn, PairTerm, PiDefn, PiSymbolicFunc, PlusTyp, FirstIncl, InducFn, RecFn, ScndIncl, ProdTyp, InducFn, RecFn, Prop, RecFunc, Refl, SigmaTyp, InducFn, RecFn, SmallTyp, Star, SymbEquality, SymbObj, SymbProp, SymbTyp, Symbolic, SymbolicFunc, Term, Typ, Unit, InducFn, RecFn, Universe, Zero, InducFn, RecFn, Factorize, Quotient, Truncation, IndTyp, Funcs, Funcs, InductiveDefinition, DataCons, Empty, RecursiveDefinition, DataCons, Empty, SmallBool, SmallNat, InductiveTyp, InductiveTypDefinition, Bool, Bool, isTrueTyp, yes, EnumTerm, EnumTyp, FreeGroup, IndexedVecTyp, Fin, IntTyp, N, Z, IntVector, ListTyp, ListTerm, ListTyp, Induc, Rec, NatTypLong, PlusExtendedDepFunction, PlusExtendedFunction, Pos, PosLiteral, PosWit, PosWitProd, PosWitSum, PosZero, SymbPosWit, RepTerm, ExtendedDepFunction, ExtendedFunction, ConstTerm, ExtendedDepFunction, ExtendedFunction, NatInt, RepSymbObj, SimpleConst, SimpleExtendedFunction, ScalaTyp, ScalaTypUniv, FineSymbTyp, FineUniv, FuncTypUniv, HigherUniv, VecTyp, SymbScalaTyp, AddLiteral, AddTerm, AdditiveMorphism, Homomorphism, LocalTyp, PiTerm, SigmaTerm, multLiteral, multTerm, prod, sum, SymbolicGroup, MultLiteral, MultTerm, inv, mul, VecTyp, FoldedTerm, PiTyp, PiTypUniv
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Subs
  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

Abstract Value Members

  1. abstract def newobj: U with Subs[U]

    A new object with the same type, to be used in place of a variable to avoid name clashes.

    A new object with the same type, to be used in place of a variable to avoid name clashes. Should throw exception when invoked for constants.

  2. abstract def subs(x: Term, y: Term): U with Subs[U]

    substitute x by y recursively in this.

Concrete Value Members

  1. def replace(x: Term, y: Term): U with Subs[U]

    refine substitution so if x and y are both of certain forms such as pairs or formal applications, components are substituted.