(*Generated by Lem from tuple.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_tuple"

 

(*open import Bool Basic_classes*)

(* ----------------------- *)
(* fst                     *)
(* ----------------------- *)

(*val fst : forall 'a 'b. 'a * 'b -> 'a*)
(*let fst (v1, v2)=  v1*)

(* ----------------------- *)
(* snd                     *)
(* ----------------------- *)

(*val snd : forall 'a 'b. 'a * 'b -> 'b*)
(*let snd (v1, v2)=  v2*)


(* ----------------------- *)
(* curry                   *)
(* ----------------------- *)

(*val curry : forall 'a 'b 'c. ('a * 'b -> 'c) -> ('a -> 'b -> 'c)*)

(* ----------------------- *)
(* uncurry                 *)
(* ----------------------- *)

(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*)


(* ----------------------- *)
(* swap                    *)
(* ----------------------- *)

(*val swap : forall 'a 'b. ('a * 'b) -> ('b * 'a)*) 
(*let swap (v1, v2)=  (v2, v1)*)

val _ = export_theory()