Lines Matching refs:pair
38 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
39 { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
66 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
67 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
80 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
81 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
92 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
93 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
94 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
95 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
99 { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },