--- Day changed Sat Feb 04 2017
TanebIs it possibly to have a type something like (b : B a) -> (a : A) -> C04/02 11:03
TanebThat is, a function with the first parameter depending on the second04/02 11:03
drdoTaneb: That would mean that the second argument isn't an argument at all, it's determined by the first argument.04/02 11:11
mudriTaneb: Agda has syntax declarations, which are slightly more general than mixfix declarations in that arguments can be re├Ârdered arbitrarily.04/02 15:03
mudriSee Data.Product.04/02 15:03
Tanebmudri, thanks, I think that's what I want04/02 15:04
mietekTaneb: yes04/02 20:15

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