--- Day changed Mon Jul 10 2017
arjen-jonathanHi all10/07 13:59
arjen-jonathanWhat is the reason that the sized version of the partiality monad is not in agda-stdlib?10/07 13:59
rntzI'm using records with constructors in agda, eg. (record Foo : Set1 where constructor make-foo; field get-foo : Set1), and when I ask for the type of a hole, I'm seeing something strange10/07 15:06
rntzwhere the type it expects involves a Foo10/07 15:07
rntzbut it writes (make-foo (get-foo a)), where `a` is some Foo in context10/07 15:07
rntzbut (make-foo (get-foo a)) is surely just `a`?10/07 15:07
rntzanyone know why it might be doing that?10/07 15:07
rntzthis is making the types of my holes huge and unreadable10/07 15:08
rntzI have to copy them into a temporary buffer and manually edit them until they're clearer :(10/07 15:08
Saizanrntz: have you tried pattern matching against a with make-foo? it should help a bit10/07 16:22
Saizanrntz: I mean, Agda sometimes eta-expands to help with conversion checking however if you have some example where it's annoying it would be nice to see if it's a bug there.10/07 16:24
rntz`a` is an implicit argument in this case, so having to pattern-match against it is kinda defeating the purpose, but I guess I could try that10/07 17:10
rntzI should probably try to minimize this test case10/07 17:12
rntzI should also update to a more recent agda10/07 17:12
rntzand see whether the prolem is still present10/07 17:12
rntzhm, how do I declare infix an operator I've imported from another module but renamed10/07 20:05
rntzlike, "open MyModule renaming (foo to _*_)"10/07 20:05
rntzhow do I declare the fixity of _*_?10/07 20:05
mietekrntz: I’m afraid you don’t; define a new one10/07 23:49

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