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

   Definition Classes

   InternalDeclaration

5.  def applyInstanciated(args: Context, params: List[Term])(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

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

   Definition Classes

   InternalDeclaration

7.  def applyTo(tm: Term)(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

8.  def applyTo(args: Context)(implicit parent: GlobalName): Term

   Definition Classes

   InternalDeclaration

9.  def applyTo(args: List[Term])(implicit parent: GlobalName): Term

   apply the internal declaration to the given argument context

   apply the internal declaration to the given argument context

   Definition Classes

   InternalDeclaration

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

    Definition Classes

    InternalDeclaration

11.  val args: List[(Option[LocalName], Term)]

    Definition Classes

    TypeLevel → InternalDeclaration

12.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

13.  def clone(): AnyRef

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()

14.  def context: Context

    Definition Classes

    InternalDeclaration

15.  val ctx: Option[Context]

    Definition Classes

    TypeLevel → InternalDeclaration

16.  val df: Option[Term]

    Definition Classes

    TypeLevel → InternalDeclaration

17.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

18.  def externalDf(implicit parent: GlobalName): Option[Term]

    like df but with all names externalized

    like df but with all names externalized

    Definition Classes

    InternalDeclaration

19.  def externalPath(implicit parent: GlobalName): GlobalName

    like path but with externalized path

    like path but with externalized path

    Definition Classes

    InternalDeclaration

20.  def externalRet(implicit parent: GlobalName): Term

    Definition Classes

    InternalDeclaration

21.  def externalTp(implicit parent: GlobalName): Term

    like tp but with all names externalized

    like tp but with all names externalized

    Definition Classes

    InternalDeclaration

22.  def finalize(): Unit

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

23.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

24.  def internalTp: Term

    Definition Classes

    InternalDeclaration

25.  def isConstructor: Boolean

    Definition Classes

    InternalDeclaration

26.  def isIndependentArgument(arg: (Option[LocalName], Term)): Boolean

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

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

    Definition Classes

    InternalDeclaration

27.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

28.  def isOutgoing: Boolean

    Definition Classes

    InternalDeclaration

29.  def isSimplyTyped(): Boolean

    checks whether the declaration is simply typed

    checks whether the declaration is simply typed

    Definition Classes

    InternalDeclaration

30.  def isTypeLevel: Boolean

    Definition Classes

    TypeLevel → InternalDeclaration

31.  def makeVar(name: String, con: Context)(implicit parent: GlobalName): VarDecl

    a var decl with a fresh name whose type is this one

    a var decl with a fresh name whose type is this one

    name

    a suggestion for the name of the new variable

    con

    a context of arguments to apply the tpl to (other than the context)

32.  def name: LocalName

    Definition Classes

    InternalDeclaration

33.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

34.  val notC: Option[NotationContainer]
35.  def notation: NotationContainer

    Definition Classes

    TypeLevel → InternalDeclaration

36.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

37.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

38.  val path: GlobalName

    Definition Classes

    TypeLevel → InternalDeclaration

39.  def ret: Term

    Definition Classes

    TypeLevel → InternalDeclaration

40.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

41.  def tm: Option[Term]
42.  def toConstant(implicit parent: GlobalName): Constant

    Definition Classes

    InternalDeclaration

43.  def toConstant(simplifyTag: Boolean)(implicit parent: GlobalName): Constant

    Definition Classes

    InternalDeclaration

44.  def toString(): String

    Definition Classes

    InternalDeclaration → AnyRef → Any

45.  def toString(termPresenter: Option[(Term) ⇒ String]): String

    Definition Classes

    InternalDeclaration

46.  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

    Definition Classes

    InternalDeclaration

47.  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

    Definition Classes

    InternalDeclaration

48.  def toVarDecl: VarDecl

    Definition Classes

    InternalDeclaration

49.  def tp: Term

    Definition Classes

    InternalDeclaration

50.  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

    Definition Classes

    InternalDeclaration

51.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

52.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

53.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()