Lem_tuple.thy

chapter \<open>Generated by Lem from \<open>tuple.lem\<close>.\<close>

theory "Lem_tuple" 

imports
  Main
  "Lem_bool"
  "Lem_basic_classes"

begin 

 

(*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)*)

end