The Theory pair
 Parents
 misc
 Children
 ℕ
 Constants
 IsPairRep ('a → 'b → BOOL) → BOOL \$, 'a → 'b → 'a × 'b Fst 'a × 'b → 'a Snd 'a × 'b → 'b Uncurry ('a → 'b → 'c) → 'a × 'b → 'c Curry ('a × 'b → 'c) → 'a → 'b → 'c Pair ('a → 'b) × ('a → '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 comma_def ⊢ ∃ fst snd • (∀ 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) fst_def ⊢ ∃ snd • (∀ 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) , Fst Snd pair_ops_def snd_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) Pair pair_def ⊢ ∀ f g• Pair (f, g) = (λ x• (f x, g x))
 Theorems
 pair_clauses ⊢ ∀ x y a b p fu fc fg • 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) ∧ Pair fg x = (Fst fg x, Snd fg x)