Package pair: Product types

Information

namepair
version1.20
descriptionProduct types
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
showData.Bool
Data.Pair

Files

Defined Type Operator

Defined Constants

Theorems

xy. (fst xy, snd xy) = xy

x y. fst (x, y) = x

x y. snd (x, y) = y

xy. x y. xy = (x, y)

p. (xy. p xy) x y. p (x, y)

p. (xy. p xy) x y. p (x, y)

p. (x y. p (x, y)) xy. p xy

f. fn. x y. fn (x, y) = f x y

f. (λxy. f xy) = λ(x, y). f (x, y)

x y a b. (x, y) = (a, b) x = a y = b

p. ((x, y). p x y) x y. p x y

p. ((x, y). p x y) x y. p x y

p. ((x, y, z). p x y z) x y z. p x y z

p. ((x, y, z). p x y z) x y z. p x y z

Input Type Operators

Input Constants

Assumptions

¬

¬

t. t t

p. p

t. t ¬t

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

p x. p x p ((select) p)

f y. (let x y in f x) = f y

x y. x = y y = x

t1 t2. t1 t2 t2 t1

() = λp q. (λf. f p q) = λf. f

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

t1 t2 t3. (t1 t2) t3 t1 t2 t3

p x. (y. p y y = x) (select) p = x

p. (x. y. p x y) y. x. p x (y x)

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x