--- Day changed Tue Apr 11 2017
quchenCan I make Agda more »eager« to use nice number displaying? Despite defining my Nat type as built-in, and seeing nice numbers like »3« sometimes, I still get long chains of »succ (succ (succ zero))« all over the place.11/04 09:53
quchene.g. https://imgur.com/a/flXCO11/04 09:55
quchenThanks for the continued help in this channel by the way :-) Really enjoying Agda so far11/04 09:56
gallaisquchen: there's a patch in the current dev version folding nats: https://github.com/agda/agda/commit/a00cc1d58f5d32e1c5bf8cf371a3dfbedabd21c911/04 10:21
quchengallais: Ah, that’s nice to know. Although I don’t understand the issue text very well: the last sentence seems to claim the entire issue is not useful.11/04 11:18
gallaisquchen: basically if "zero" is alone, it won't get folded. But any stack of sucs will11/04 11:57
quchengallais: But in my screenshot, I have a stack of succs, but they don’t get folded.11/04 11:58
quchenOr is what you mentioned the is-state, not the should-state?11/04 11:58
gallaisthe patch is *in the current dev version* so if you won't benefit from it until the next release (or if you install a dev version of Agda)11/04 12:01
gallaiss/if you won't/you won't/11/04 12:01
mietekgallais: cool!11/04 18:35

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