Packages

object InducPairs

Recursion and induction for (dependent) pairs.

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

Value Members

  1. val A: Typ[Term]
  2. val B: Typ[Term]
  3. val Bs: Func[Term, Typ[Term]]
  4. val Btype: PiDefn[Term, Term]
  5. val C: Typ[Term]
  6. val Cs: Func[Term, Func[Term, Typ[Term]]]
  7. val InducSigma: FuncLike[Typ[Term], FuncLike[Func[Term, Typ[Term]], FuncLike[Func[Term, Func[Term, Typ[Term]]], FuncLike[FuncLike[Term, FuncLike[Term, Term]], FuncLike[AbsPair[Term, Term], Term]]]]]
  8. val a: Term
  9. val ab: PairTerm[Term, Term]
  10. val abDep: AbsPair[Term, Term]
  11. val b: Term
  12. val bs: FuncLike[Term, Term]
  13. val f: Func[Term, Func[Term, Term]]
  14. val g: FuncLike[Term, Func[Term, Term]]
  15. val h: FuncLike[Term, FuncLike[Term, Term]]
  16. val hDep: FuncLike[Term, FuncLike[Term, Term]]
  17. val inducPair: FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[Func[Term, Func[Term, Typ[Term]]], FuncLike[FuncLike[Term, FuncLike[Term, Term]], FuncLike[PairTerm[Term, Term], Term]]]]]
  18. val recPair: FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[Func[Term, Func[Term, Term]], FuncLike[PairTerm[Term, Term], Term]]]]]
  19. val recSigma: FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[Typ[Term], FuncLike[FuncLike[Term, Func[Term, Term]], FuncLike[AbsPair[Term, Term], Term]]]]]
  20. val toC: GenFuncTyp[Term, Func[Term, Term]]
  21. val toCs: GenFuncTyp[Term, FuncLike[Term, Term]]
  22. val toCsDep: GenFuncTyp[Term, FuncLike[Term, Term]]