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

--- Day changed Sat Feb 18 2017
wedifyi hope agda will support overloaded literals in the future. Sign.+ ◃ 1 is retarded18/02 00:10
wedifyis there a better way to make an integer from a nat?18/02 00:10
TanebWhy not just +_ ?18/02 00:18
TanebOr am I misremembering18/02 00:18
TanebYeah, +_ is one of the constructors for integers18/02 00:19
wedifyah. so then to create a negative integer i go -(+ 1)18/02 00:21
wedifyweird but acceptable18/02 00:21
TanebOr you could use the -[1+_] constructor if it's convenient18/02 00:22
wedifyTaneb: that requires a whole extra character :P18/02 00:25
subttle-- Is it possible to write an instance for DistributesOver using Nat's _*_ and _+_ I'm struggling to see how to line up the types :/ if anyone could find the time to explain how this could be done I would appreciate it (I could only find one example and it was not the most helpful for me)18/02 06:58
subttleI don't understand why I can't use:18/02 07:02
subttleexample : ? DistributesOverˡ ?18/02 07:02
subttleWhy do I get a Type Mismatch on a hole?18/02 07:04
glguysubttle: Perhaps you imported FunctionProperties directly and need to provide an equality relation argument18/02 07:18
subttleglguy: Bingo18/02 07:19
subttleyou are amazing18/02 07:19
subttlethank you18/02 07:20
subttlethe other properties let me provide it as an argument, but I guess it is better to explicitly open it with the equality relation!!18/02 07:22
mckeankylejhow do i input the level maximum unicode char in emacs?18/02 21:52
mckeankylejapparently there is an emacs command to search for char input methods18/02 21:54
mckeankylejsorry for the silly question18/02 21:55

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