sealed abstract class InternalDeclaration extends AnyRef

helper class for the various declarations in an inductive type

Source
InternalDeclaration.scala
Linear Supertypes
AnyRef, Any
Known Subclasses
Constructor, OutgoingTermLevel, StatementLevel, TermLevel, TypeLevel
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. InternalDeclaration
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract def args: List[(Option[LocalName], Term)]
  2. abstract def ctx: Option[Context]
    Attributes
    protected
  3. abstract def df: Option[Term]
  4. abstract def isTypeLevel: Boolean
  5. abstract def notation: NotationContainer
  6. abstract def path: GlobalName
  7. abstract def ret: Term

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def applyInstanciated(arg: Term, params: List[Term])(implicit parent: GlobalName): Term
  5. def applyInstanciated(args: Context, params: List[Term])(implicit parent: GlobalName): Term
  6. def applyInstanciated(args: List[Term], params: List[Term])(implicit parent: GlobalName): Term

    apply the internal declaration to the given argument context and with its context instanciated to the given parameters

    apply the internal declaration to the given argument context and with its context instanciated to the given parameters

    args

    the arguments to apply the internal declaration to

    params

    the parameters to instanciate the context to

    parent

    (implicit) the path of the parent derived declaration

  7. def applyTo(tm: Term)(implicit parent: GlobalName): Term
  8. def applyTo(args: Context)(implicit parent: GlobalName): Term
  9. def applyTo(args: List[Term])(implicit parent: GlobalName): Term

    apply the internal declaration to the given argument context

  10. def argContext(suffix: Option[String] = None)(implicit parent: GlobalName): (Context, Term)

    Build a context quantifying over all arguments and the term of this constructor applied to those arguments

    Build a context quantifying over all arguments and the term of this constructor applied to those arguments

    suffix

    (optional) a suffix to append to the local name of each independent variable declaration in the returned context

  11. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  12. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  13. def context: Context
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  16. def externalDf(implicit parent: GlobalName): Option[Term]

    like df but with all names externalized

  17. def externalPath(implicit parent: GlobalName): GlobalName

    like path but with externalized path

  18. def externalRet(implicit parent: GlobalName): Term
  19. def externalTp(implicit parent: GlobalName): Term

    like tp but with all names externalized

  20. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  21. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  22. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  23. def internalTp: Term
  24. def isConstructor: Boolean
  25. def isIndependentArgument(arg: (Option[LocalName], Term)): Boolean

    checks whether the type of the declaration is dependent on the given argument

  26. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  27. def isOutgoing: Boolean
  28. def isSimplyTyped(): Boolean

    checks whether the declaration is simply typed

  29. def name: LocalName
  30. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  31. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  32. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  33. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  34. def toConstant(implicit parent: GlobalName): Constant
  35. def toConstant(simplifyTag: Boolean)(implicit parent: GlobalName): Constant
  36. def toString(): String
    Definition Classes
    InternalDeclaration → AnyRef → Any
  37. def toString(termPresenter: Option[(Term) ⇒ String]): String
  38. def toTerm(implicit parent: GlobalName): Term

    apply the internal declaration to its context

    apply the internal declaration to its context

    parent

    (implicit) the path of the parent derived declaration

  39. def toTermInstanciated(params: List[Term])(implicit parent: GlobalName): Term

    apply the internal declaration to a list of parameters instanciating its context

    apply the internal declaration to a list of parameters instanciating its context

    params

    the parameters to instanciate the context to

    parent

    (implicit) the path of the parent derived declaration

  40. def toVarDecl: VarDecl
  41. def tp: Term
  42. def translate(tr: Translator): InternalDeclaration

    applies a term translator to the arguments and definien of an internal declaration

    applies a term translator to the arguments and definien of an internal declaration

    tr

    the translator to apply

  43. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  44. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  45. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from AnyRef

Inherited from Any

Ungrouped