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

--- Day changed Sat Jan 21 2017
Saizan_the /r/agda subreddit needs an active mod to deal with the spam, anyone with 500+ combined karma who would like to request for mod powers?21/01 14:11
Saizan_https://www.reddit.com/r/redditrequest/about/sidebar21/01 14:11
akrSaizan_: sure, why not21/01 17:46
akrah, looks like someone's already up to it21/01 17:48
mietekYou can submit an URL again with ?something=added21/01 21:34
rgrinbergIs there a way to import syntax from  an agda module?21/01 22:07
mietekrgrinberg: import the symbol for which the syntax is defined.21/01 22:45
mietekrgrinberg: take a look how it’s done here: https://agda.github.io/agda-stdlib/Data.Product.html#43921/01 22:46
mietekΣ-syntax is an explicit alias for Σ; when you Σ-syntax you get the syntax as well21/01 22:46
mietekwhen you import*21/01 22:46

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