chapter ‹Generated by Lem from ‹tuple.lem›.› 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