Packages

package lkt

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

Type Members

  1. trait ALCtx[LC <: ALCtx[LC]] extends AnyRef
  2. case class AllL(main: Hyp, term: Expr, q: Bound1) extends LKt with Product with Serializable
  3. case class AllR(main: Hyp, ev: Var, q: Bound1) extends LKt with Product with Serializable
  4. case class AllSk(main: Hyp, term: Expr, q: Bound1) extends LKt with Product with Serializable
  5. case class AndL(main: Hyp, q: Bound2) extends LKt with Product with Serializable
  6. case class AndR(main: Hyp, q1: Bound1, q2: Bound1) extends LKt with Product with Serializable
  7. case class Ax(main1: Hyp, main2: Hyp) extends LKt with Product with Serializable
  8. trait B1[LC <: ALCtx[LC]] extends AnyRef
  9. trait B2[LC <: ALCtx[LC]] extends AnyRef
  10. trait BN[LC <: ALCtx[LC]] extends AnyRef
  11. trait Bound extends AnyRef
  12. final case class Bound1(aux: Hyp, p: LKt) extends Bound with Product with Serializable
  13. final case class Bound2(aux1: Hyp, aux2: Hyp, p: LKt) extends Bound with Product with Serializable
  14. final case class BoundN(auxs: List[Hyp], p: LKt) extends Bound with Product with Serializable
  15. case class Cut(f: Formula, q1: Bound1, q2: Bound1) extends LKt with Product with Serializable
  16. case class Def(main: Hyp, f: Formula, q: Bound1) extends LKt with Product with Serializable
  17. case class Eql(main: Hyp, eq: Hyp, ltr: Boolean, rwCtx: Expr, q: Bound1) extends LKt with Product with Serializable
  18. class FakeLocalCtx extends ALCtx[FakeLocalCtx]
  19. trait FreshHyp extends AnyRef
  20. final case class Hyp(idx: Int) extends AnyVal with Product with Serializable
  21. implicit final class HypSet extends AnyVal
  22. trait ImplicitInstances extends AnyRef
  23. case class Ind(main: Hyp, f: Abs, term: Expr, cases: List[IndCase]) extends LKt with Product with Serializable
  24. case class IndCase(ctr: Const, evs: List[Var], q: BoundN) extends Product with Serializable
  25. class LKToLKt extends FreshHyp
  26. sealed trait LKt extends AnyRef
  27. case class Link(mains: List[Hyp], name: Expr) extends LKt with Product with Serializable
  28. case class LocalCtx(hyps: Map[Hyp, Formula], subst: Substitution) extends ALCtx[LocalCtx] with Product with Serializable
  29. case class NegL(main: Hyp, q: Bound1) extends LKt with Product with Serializable
  30. case class NegR(main: Hyp, q: Bound1) extends LKt with Product with Serializable
  31. class Normalizer[LC <: ALCtx[LC]] extends AnyRef
  32. class NormalizerWithDebugging extends Normalizer[LocalCtx]
  33. case class Rfl(main: Hyp) extends LKt with Product with Serializable
  34. trait SimpAdapter extends AnyRef
  35. case class SimplifierSimpAdapter(simp: Simplifier, lctx: LocalCtx) extends SimpAdapter with Product with Serializable
  36. case class TopR(main: Hyp) extends LKt with Product with Serializable
  37. class makeEqualityExplicit extends FreshHyp
  38. class normalize extends AnyRef
  39. class unfoldInduction extends AnyRef

Value Members

  1. implicit val closedUnderSubstitution: ClosedUnderSub[LKt]
    Definition Classes
    ImplicitInstances
  2. implicit val closedUnderSubstitutionBound1: ClosedUnderSub[Bound1]
    Definition Classes
    ImplicitInstances
  3. implicit val closedUnderSubstitutionBound2: ClosedUnderSub[Bound2]
    Definition Classes
    ImplicitInstances
  4. implicit val closedUnderSubstitutionBoundN: ClosedUnderSub[BoundN]
    Definition Classes
    ImplicitInstances
  5. implicit val closedUnderSubstitutionIndCase: ClosedUnderSub[IndCase]
    Definition Classes
    ImplicitInstances
  6. object AllL extends Serializable
  7. object AllLBlock
  8. object AllR extends Serializable
  9. object AllRBlock
  10. object AllSk extends Serializable
  11. object AndL extends Serializable
  12. object AndR extends Serializable
  13. object BinConn
  14. object Cut extends Serializable
  15. object Def extends Serializable
  16. object Eql extends Serializable
  17. case object FakeLocalCtx extends FakeLocalCtx with Product with Serializable
  18. object Hyp extends Serializable
  19. implicit object replaceable extends ClosedUnderReplacement[LKt]
    Definition Classes
    ImplicitInstances
  20. implicit object replaceableBnd1 extends ClosedUnderReplacement[Bound1]
    Definition Classes
    ImplicitInstances
  21. implicit object replaceableBnd2 extends ClosedUnderReplacement[Bound2]
    Definition Classes
    ImplicitInstances
  22. implicit object replaceableBndN extends ClosedUnderReplacement[BoundN]
    Definition Classes
    ImplicitInstances
  23. implicit object replaceableIndCase extends ClosedUnderReplacement[IndCase]
    Definition Classes
    ImplicitInstances
  24. object LKToLKt
  25. object LKtToLK
  26. object LocalCtx extends Serializable
  27. object NegL extends Serializable
  28. object NegR extends Serializable
  29. case object NoopSimpAdapter extends SimpAdapter with Product with Serializable
  30. object atomizeEquality
  31. object check
  32. object makeEqualityExplicit
  33. object normalize extends normalize
  34. object unfoldInduction

Inherited from ImplicitInstances

Inherited from AnyRef

Inherited from Any

Ungrouped