Packages

p

gapt

expr

package expr

Source
package.scala
Linear Supertypes
AnyRef, Any
Content Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. expr
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Package Members

  1. package formula
  2. package subst
  3. package ty
  4. package util

Type Members

  1. class Abs extends Expr
  2. class App extends Expr
  3. type ClosedUnderFOLSub[T] = Substitutable[FOLSubstitution, T, T]
  4. type ClosedUnderReplacement[T] = Replaceable[T, T]
  5. type ClosedUnderSub[T] = Substitutable[Substitution, T, T]
  6. class Const extends Expr with VarOrConst
  7. abstract class Expr extends AnyRef
  8. implicit final class ExprNameGenerator extends AnyVal
  9. case class Normalizer(rules: Set[ReductionRule]) extends Product with Serializable
  10. case class ReductionRule(lhs: Expr, rhs: Expr) extends Product with Serializable
  11. trait Replaceable[-I, +O] extends AnyRef
  12. trait ReplaceableInstances0 extends AnyRef
  13. trait ReplaceableInstances1 extends ReplaceableInstances0
  14. trait ReplaceableInstances2 extends ReplaceableInstances1
  15. type ReplacementContext = Abs
  16. class Var extends Expr with VarOrConst
  17. trait VarOrConst extends Expr

Value Members

  1. implicit def stringInterpolationForExpressions(sc: StringContext)(implicit file: File, line: Line, sig: BabelSignature): ExpressionParseHelper
  2. object Abs
  3. object App
  4. object Apps
  5. object BetaReduction extends Normalizer
  6. object Const
  7. object Normalizer extends Serializable
  8. object ReductionRule extends Serializable
  9. object Replaceable extends ReplaceableInstances2
  10. object TermReplacement

    A term replacement homomorphically extends a partial function on lambda expressions to all lambda expressions.

    A term replacement homomorphically extends a partial function on lambda expressions to all lambda expressions.

    This is done on a "best effort" basis. Replacing constants by ground terms of the same type will usually work, anything beyond that might or might not work.

  11. object Var
  12. object VarOrConst

    Matches constants and variables, but nothing else.

  13. object containedNames
  14. object normalize
  15. object preExpr

    Intermediate representation for expressions without explicit types.

    Intermediate representation for expressions without explicit types.

    The main application is during parsing: the gapt.formats.babel.BabelParser produces pre-expressions.

    This representation is intended to be as simple as possible, all higher-level constructs (such as <-> or ∀) are already desugared into simply-typed lambda terms.

    It differs from the "real" lambda calculus in gapt.expr in three major ways:

    1. There are type meta-variables.
    2. There are type annotations.
    3. Free variables, bound variables, and constants are not distinguished; they are all stored as "identifiers".

Inherited from AnyRef

Inherited from Any

Ungrouped