--- Day changed Sat Mar 11 2017
canndrewhow can I make agda give me a detailed description of a type error?11/03 09:17
canndrewlike, a backtrace of the unification procedure whoch explains exactly where a type error is coming from.11/03 09:17
gallaiscanndrew: You should try to pass "-vtc.lhs.unify:N" where N is the level of details you want (10 to 100 by increments of 10)11/03 09:29
gallaisit's debugging info though so it will be pretty brutal11/03 09:29
gallaisyou can learn more about these options by grepping the source code for "reportSLn"11/03 09:30
gallaisor "reportSDoc" and seeing the keys that are used to classify these debugging info11/03 09:31
canndrewgallais: thanks!11/03 09:55
augurhm11/03 10:00
augurso i figured out a way to solve my generative-recursion problem in a way that's i guess structurally recursive?11/03 10:01
augurat least enough for agda to not complain11/03 10:01
augurnamely, there are a bunch of safe unfolds that use bounds on the coalgebra carrier to "count down" so to speak11/03 10:14
augurso like stuff like this https://gist.github.com/psygnisfive/8043bdb0f8c0f1a2fe200ddc45124ff211/03 10:17
augurand i suspect that you can use this kind of bounded coalgebra in combination w/ Conor's TVFTL style programming to be able to write generatively recursive programs without it being non-obviously terminating, but also while looking like normal generatively recursive programs11/03 10:20
canndrewgiven (f = g) and (x = y) I want to prove that (f x) = (g y). How can I do that for dependent functions?11/03 13:40
mudricanndrew: I guess you state it with careful use of subst. I'll have a go...11/03 14:22
lpaste_mudri pasted “canndrew” at http://lpaste.net/35341411/03 14:29
canndrewmudri: thanks! that's what I had written but I thought it wasn't working.11/03 14:49
canndrewbut then it turned out i just didn't understand the error msg11/03 14:50
canndrewis there a way to tell auto mode to just keep searching? I'm trying to use it now but it immediately returns with "No solution found"11/03 17:58
akr[m]you can extend the timeout by typing '-t <seconds>' into the hole before starting auto11/03 18:25
akr[m]but if it fails immediatelly, it's not going to help11/03 18:26

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