Hot on the tail of Andrew Bromage's free theorems
plugin for Lambdabot, we now have two free theorem generators, thanks to
Janis Voigtlaender and Sascha Boehme's FT tool.
lambdabot> ft map
forall T1,T2 in TYPES. forall h1 :: T1 -> T2, h1 strict.
forall T3,T4 in TYPES. forall h2 :: T3 -> T4, h2 strict.
forall f1 :: T1 -> T3.
forall g1 :: T2 -> T4.
(forall x2 :: T1.
h2 (f1 x2) = g1 (h1 x2))
==> forall x1 :: [T1].
map h2 (t1 f1 x1) = t1 g1 (map h1 x1)
lambdabot> ft foldl1
forall T1,T2 in TYPES. forall h1 :: T1 -> T2, h1 strict.
forall f1 :: T1 -> T1 -> T1.
forall g1 :: T2 -> T2 -> T2.
(forall x2 :: T1.
forall x3 :: T1.
h1 (f1 x2 x3) = g1 (h1 x2) (h1 x3))
==> forall x1 :: [T1].
h1 (t1 f1 x1) = t1 g1 (map h1 x1)
/home ::
/haskell ::
permalink ::
rss
