Commit dec8d060 authored by Vincent Zweije's avatar Vincent Zweije
Browse files

Define mapsnd3

parent e1479b2e
......@@ -118,6 +118,9 @@ mappair :: .(.a -> .b) .(.c -> .d) !(.a,.c) -> (.b,.d)
// Map a function onto the second element of a 2-tuple.
mapsnd :: v:(.a -> .b) -> u:((.c,.a) -> (.c,.b)), [u <= v]
// Map a function on the second element of a triple.
mapsnd3 :: v:(.a -> .b) -> u:((.c,.a,.d) -> (.c,.b,.d)), [u <= v]
// Map a function onto the tail of a list.
maptl :: .(x:[.a] -> u:[.a]) !w:[.a] -> v:[.a], [u <= v, w <= x]
......
......@@ -198,6 +198,9 @@ mappair f g (x,y) = (f x,g y)
mapsnd :: v:(.a -> .b) -> u:((.c,.a) -> (.c,.b)), [u <= v]
mapsnd f = app2 (id,f)
mapsnd3 :: v:(.a -> .b) -> u:((.c,.a,.d) -> (.c,.b,.d)), [u <= v]
mapsnd3 f = app3 (id,f,id)
maptl :: .(x:[.a] -> u:[.a]) !w:[.a] -> v:[.a], [u <= v, w <= x]
maptl f [] = []
maptl f [x:xs] = [x:f xs]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment