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

--- Day changed Sat Aug 12 2017
glguyWhy isn't this definition accepted by the termination checker? if I pull these recursive calls out from under their functions it passes due to the lexicographic termination order, and if I write this definition using Induction.Lexicographic it works out, but this direct version doesn't : http://imgur.com/a/z9Xr012/08 02:49
glguyWeird, it allows it if I move one of the calls up into a with clause:12/08 02:57
glguyx@(limit {A} f) ⊗ y@(limit {B} g) with (λ i → x ⊗ g (proj₂ i) ⊕ f (proj₁ i) )12/08 02:57
glguy... | recˡ = limit recˡ ⊔ limit recʳ12/08 02:57
carterglguy: termination checking is voodoooo12/08 03:03
glguyIsn't there a parameter I can tune to get the checker to look a little harder?12/08 03:04
glguyI was thinking of --termination-depth=N, but it didn't help12/08 03:12

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