The Theory pair
Parents

misc
Children

Constants
IsPairRep
('a 'b BOOL) BOOL
Snd
('a 'b) 'b
Fst
('a 'b) 'a
$,
'a 'b 'a 'b
Uncurry
('a 'b 'c) ('a 'b) 'c
Curry
(('a 'b) 'c) 'a 'b 'c
Types
'1 '2
Fixity

Infix 150:,
Terminators

Definitions
IsPairRep
is_pair_rep_def
comma mk_var("fst", (('a 'b BOOL) 'a))
mk_var("snd", (('a 'b BOOL) 'b))
( x y
IsPairRep (comma x y)
mk_var("fst", (('a 'b BOOL) 'a))
(comma x y)
= x
mk_var("snd", (('a 'b BOOL) 'b))
(comma x y)
= y)
( x y a b
comma a b = comma x y a = x b = y)
( p
IsPairRep p
comma
(mk_var("fst", (('a 'b BOOL)
'a))
p)
(mk_var("snd", (('a 'b BOOL)
'b))
p)
= p)
_def
f TypeDefn IsPairRep f
,
Fst
Snd
pair_ops_def
( x y Fst (x, y) = x Snd (x, y) = y)
( x y a b (a, b) = (x, y) a = x b = y)
( p (Fst p, Snd p) = p)
Uncurry
uncurry_def
f x y Uncurry f (x, y) = f x y
Curry
curry_def
f x y Curry f x y = f (x, y)
Theorems
pair_clauses
x y a b p fu fc
Fst (x, y) = x
Snd (x, y) = y
((a, b) = (x, y) a = x b = y)
(Fst p, Snd p) = p
Curry fc x y = fc (x, y)
Uncurry fu (x, y) = fu x y
Uncurry fu p = fu (Fst p) (Snd p)
((a, b) = p a = Fst p b = Snd p)
(p = (a, b) Fst p = a Snd p = b)

up quick index © RBJ