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

--- Day changed Sun May 07 2017
acertaindoes anyone have any clue how to do dependent lists?07/05 02:57
acertainlike something that could be instantiated to get something like `data Env : Set where empty : Env; snoc : (e : Env) -> Type e -> Env`07/05 02:58
mietekacertain: telescopes?07/05 03:04
mietekacertain: https://gist.github.com/copumpkin/419701207/05 03:05
{AS}mietek: is _ an implicit conversion?07/05 12:20
{AS}It looks fairly magical to me07/05 12:20
{AS}Oh, never mind, it's a font issue07/05 12:22
mietekI just googled that07/05 12:24

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