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

    TermLevel → 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

    TermLevel → InternalDeclaration

16.  val df: Option[Term]

    Definition Classes

    TermLevel → 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 injDecls(simplifyTag: Boolean = false)(implicit parent: GlobalName): List[Constant]

    Generate injectivity declaration for the term constructor d

    Generate injectivity declaration for the term constructor d

    parent

    the parent declared module of the derived declaration to elaborate

25.  def internalTp: Term

    Definition Classes

    InternalDeclaration

26.  def isConstructor: Boolean

    Definition Classes

    InternalDeclaration

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

28.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

29.  def isOutgoing: Boolean

    Definition Classes

    InternalDeclaration

30.  def isSimplyTyped(): Boolean

    checks whether the declaration is simply typed

    checks whether the declaration is simply typed

    Definition Classes

    InternalDeclaration

31.  def isTypeLevel: Boolean

    Definition Classes

    TermLevel → InternalDeclaration

32.  def makeVar(name: String): VarDecl

    a var decl with a fresh name of the same type as this one

33.  def name: LocalName

    Definition Classes

    InternalDeclaration

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

    Definition Classes

    AnyRef

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

    Definition Classes

    TermLevel → InternalDeclaration

37.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

38.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

39.  val path: GlobalName

    Definition Classes

    TermLevel → InternalDeclaration

40.  val ret: Term

    Definition Classes

    TermLevel → InternalDeclaration

41.  def surjDecl(simplifyTag: Boolean = false)(implicit parent: GlobalName): Constant

    Generate surjectivity declaration for the term constructor d

    Generate surjectivity declaration for the term constructor d

    parent

    the parent declared module of the derived declaration to elaborate

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

    Definition Classes

    AnyRef

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

    Definition Classes

    InternalDeclaration

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

    Definition Classes

    InternalDeclaration

46.  def toString(): String

    Definition Classes

    InternalDeclaration → AnyRef → Any

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

    Definition Classes

    InternalDeclaration

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

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

50.  def toVarDecl: VarDecl

    Definition Classes

    InternalDeclaration

51.  def tp: Term

    Definition Classes

    InternalDeclaration

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

53.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()