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

--- Day changed Wed Mar 29 2017
apostolisI have written a lot of functions for a specific data type. Then I require a stricter data type, meaning that some of the constructors are prohibited, or the dedendent conditions are more strict.29/03 12:43
apostolisIs there a way to reuse the previous functions instead of writing the same functions again?29/03 12:44
canndrewwill replacing all the implicit arguments on all my functions with explicit arguments make agda not take 5 minutes to typecheck my code?29/03 15:09
canndrewalternatively, is it possible to change agda's type-checking algorithm to something that may require a few more type annotations but can complete substantially quicker?29/03 15:32
canndrewlike a --dont-do-any-complicated-inference flag?29/03 15:55
canndrewI'm assuming inference is why it takes so long29/03 15:55
mietekcanndrew: 5 minutes?29/03 18:28
mietekcanndrew: do you use instance reolution?29/03 19:31
mietekresolution*29/03 19:31
{AS}canndrew: do you have complex code you are using in types?29/03 22:15

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