/home/laney/.irssi/irclogs/Freenode/#agda.log-20170129

--- Day changed Sat Jan 28 2017
rribeiroHi all! I'm with a little doubt. I have a goal of the form P (map (\x -> x . y . z) xs) and a hypothesis of with type P (map (\ x -> (x . y) . z) xs). Is it possible to rewrite the hypothesis to mach the goal without using function extensionality as a postulate?28/01 21:25
lpasteglguy pasted “For rribeiro” at http://lpaste.net/35175028/01 22:33
rribeiroglguy: Ohhh I forgot to say that "." is a custom operator not function composition. 28/01 22:36
rribeiroI'm looking for any tip (if there's any) to avoid axiom of function extensionality to solve something like this28/01 22:37

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!