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

--- Day changed Thu Jan 18 2018
tomjackAn internal error has occurred. Please report this as a bug.18/01 04:51
tomjackLocation of the error: src/full/Agda/TypeChecking/Primitive.hs:110418/01 04:51
tomjackhcomp <- fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinPOhcomp18/01 04:52
tomjackthis despite having loaded PushOut.agda with primitive primPushOutHComp, hmm18/01 04:53
tomjackit feels like possibly the bug is that ReduceM doesn't have primPushOutHComp, but TCMT does18/01 04:59
tomjack(just because I get the error only when attempting to normalize something pushouty)18/01 05:00
tomjackoh, well, I dunno, I can trigger the error in typechecking too18/01 05:03
tomjackhttps://www.irccloud.com/pastebin/J8mjFOIk/Flattening.agda18/01 05:03
tomjack(at the bottom)18/01 05:03
Saizantomjack: i think i fixed that shortly after, maybe pull again?18/01 08:47
tomjackhmm, I'm on 2.6.0-5d8475418/01 08:49
Saizanoh, i never pushed it!18/01 08:51
Saizantomjack: now pull again :) thanks for reporting this!18/01 08:55
tomjackah, thanks. now the error begins to make some sense to me18/01 08:56
tomjackcool, now I get the 1MB normal form I deserve18/01 09:04
Saizanlol18/01 09:11
Saizanyeah, things compute too much for my taste18/01 09:12
* Saizan still trying to find a computer-sciency example for univalence18/01 09:25
trikl[m]I want to represent a table of size `n` where each of the entries is `Fin n -> A`. I would then want to be able to apply functions to the whole table or to some particular `Fin n`. This is a functor, right? Is there anything in the stdlib I can use? 18/01 09:26
Saizantrikl[m]: have you looked at Data.Vec ?18/01 09:37
trikl[m]Oh of course18/01 09:41
trikl[m]Thanks Saizan 18/01 09:41

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