| 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 |
| Right Infix 150: |
, | |
| Terminators |
| |
| Definitions |
|
IsPairRep
is_pair_rep_def
|
  comma fst snd
  ( x y IsPairRep (comma x y)  fst (comma x y) = x snd (comma x y) = y) ( x y a b comma a b = comma x y  a = x b = y) ( p IsPairRep p  comma (fst p) (snd 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)
|
