case class StatementLevel(path: GlobalName, args: List[(Option[LocalName], Term)], df: Option[Term] = None, ctx: Option[Context] = None, notC: Option[NotationContainer] = None) extends InternalDeclaration with Product with Serializable

Rules and Judgment constructors

Source
InternalDeclaration.scala
Linear Supertypes
Serializable, Serializable, Product, Equals, InternalDeclaration, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. StatementLevel
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. InternalDeclaration
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new StatementLevel(path: GlobalName, args: List[(Option[LocalName], Term)], df: Option[Term] = None, ctx: Option[Context] = None, notC: Option[NotationContainer] = None)

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
    StatementLevel → 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
    StatementLevel → InternalDeclaration
  16. val df: Option[Term]
    Definition Classes
    StatementLevel → 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
    StatementLevel → InternalDeclaration
  31. def name: LocalName
    Definition Classes
    InternalDeclaration
  32. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  33. val notC: Option[NotationContainer]
  34. def notation: NotationContainer
    Definition Classes
    StatementLevel → InternalDeclaration
  35. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  36. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  37. val path: GlobalName
    Definition Classes
    StatementLevel → InternalDeclaration
  38. def ret: Term
    Definition Classes
    StatementLevel → InternalDeclaration
  39. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  40. def tm: Option[Term]
  41. def toConstant(implicit parent: GlobalName): Constant
    Definition Classes
    InternalDeclaration
  42. def toConstant(simplifyTag: Boolean)(implicit parent: GlobalName): Constant
    Definition Classes
    InternalDeclaration
  43. def toString(): String
    Definition Classes
    InternalDeclaration → AnyRef → Any
  44. def toString(termPresenter: Option[(Term) ⇒ String]): String
    Definition Classes
    InternalDeclaration
  45. 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
  46. 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
  47. def toVarDecl: VarDecl
    Definition Classes
    InternalDeclaration
  48. def tp: Term
    Definition Classes
    InternalDeclaration
  49. 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
  50. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  51. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  52. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from InternalDeclaration

Inherited from AnyRef

Inherited from Any

Ungrouped