Packages

o

provingground.interface

InductionSession

object InductionSession

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. InductionSession
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. val A: Typ[Term]
  2. val bots: Vector[HoTTBot]
  3. val conclusion: GenFuncTyp[RepTerm[SafeLong], Equality[Term]]
  4. val f: Func[RepTerm[SafeLong], Term]
  5. val goal: FuncTyp[FuncLike[RepTerm[SafeLong], Equality[Term]], FuncLike[RepTerm[SafeLong], Equality[Term]]]
  6. val hypothesis: GenFuncTyp[RepTerm[SafeLong], Equality[Term]]
  7. val lp: LocalProver
  8. val n: RepTerm[SafeLong]
  9. lazy val sessF: Future[HoTTWebSession]
  10. val terms: FiniteDistribution[Term]
  11. val tg: TermGenParams
  12. val ts: TermState
  13. val typs: FiniteDistribution[Typ[Term]]
  14. val web: HoTTPostWeb
  15. val ws: WebState[HoTTPostWeb, ID]
  16. lazy val wsF: Future[WebState[HoTTPostWeb, ID]]