Packages

c

info.kwarc.mmt.api.notations

SimpleFixity

abstract class SimpleFixity extends Fixity

A SimpleFixity is one out of multiple typical fixities (infix, postfix, etc) characterized by using only a single delimiter.

impl and expl do not have to agree with the number of arguments demanded by the type system. * Notation has more arguments than function type: Notation extensions may handle the extra arguments. Example: equal : {a:tp} tm (a => a => bool), impl = 1, expl = 2 * Notation has less arguments than function type: Operator return a function. Example: union : {a:tp} tm (a set => a set => a set) where a set = a => bool, impl = 1, expl = 2

Source
NotationExtension.scala
Linear Supertypes
Fixity, AnyRef, Any
Known Subclasses
Bindfix, Infix, Postfix, Prefix
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SimpleFixity
  2. Fixity
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new SimpleFixity()

Abstract Value Members

  1. abstract def addInitialImplicits(n: Int): Fixity
    Definition Classes
    Fixity
  2. abstract def asString: (String, String)

    the string representation to use when serializing notations pair of "fixity type" and type-specific argument(s)

    the string representation to use when serializing notations pair of "fixity type" and type-specific argument(s)

    Definition Classes
    Fixity
  3. abstract def delim: Delimiter

    the delimiter to use

  4. abstract def expl: Int

    expl number of subsequent explicit arguments (needed to trigger notation during parsing, rendered by printer)

  5. abstract def impl: Int

    number of initial implicit arguments (inferred by parser, skipped by printer)

  6. abstract def markers: List[Marker]

    the elaboration into markers

    the elaboration into markers

    Definition Classes
    Fixity

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 argsWithOp(beforeOp: Int): List[Marker]

    ImplicitArgs Args1 Delim Args2 with Args1.length == beforeOp

    ImplicitArgs Args1 Delim Args2 with Args1.length == beforeOp

    Attributes
    protected
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def implArgs: List[ImplicitArg]
    Attributes
    protected
  13. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  14. def isRelative: Boolean

    true if this notation can be used for multiple constants without ambiguity because it contains placeholders

    true if this notation can be used for multiple constants without ambiguity because it contains placeholders

    Definition Classes
    Fixity
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. def relativize: Option[Fixity]

    wrap first delimiter in instance name

    wrap first delimiter in instance name

    Definition Classes
    Fixity
  19. def simpleArgs: String
    Attributes
    protected
  20. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  21. def toString(): String
    Definition Classes
    AnyRef → Any
  22. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  23. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  24. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from Fixity

Inherited from AnyRef

Inherited from Any

Ungrouped