--- Day changed Tue Dec 05 2017
comietekis there any example of using the JS backend whatsoever?05/12 08:00
ninegridDoes anyone have any insight into why lowercase constructors seem to be idiomatic?  I haven't been able to find any specific explination as to why this is preferred (not that I'm complaining about it, I'm just curious)05/12 09:02
{AS}ninegrid: This is just a guess, but I would think that it is because it is idiomatic in Agda to only write types in uppercase05/12 09:03
{AS}In Haskell there is this idea of punning so constructors and types get the same name, which is possible because they are in different namespaces05/12 09:03
{AS}But in Agda, they share the same namespace so that is not possible05/12 09:04
{AS}I believe this corresponds well with mathematical style where you write sets in capital and values in minuscule  05/12 09:07
ninegrid{AS}: Thanks05/12 09:09
{AS}sure :)05/12 09:09
WilliamHamiltonpgiarrusso: hi, I tried to use an inspect idiom, but pattern matching on the resulting eq seems to not be possible because "I'm not sure if there should be a case for the constructor refl,05/12 16:46
WilliamHamiltonbecause I get stuck when trying to solve the following unification05/12 16:46
WilliamHamiltonproblems"05/12 16:46
WilliamHamiltonwhat should I do, in general terms, to solve the problem?05/12 16:46
pgiarrussoWilliamHamilton: so refl has type e1 == e2 where those don’t unify; you’ll need to use a separate, more general lemma taking a refl of a more general type (say, e1’ == e2’), where e1’ and e2’ can unify — say, because they’re variables05/12 17:15
pgiarrussoa common case where this happens when e1 and e2 have function calls; f a b = g c d, with f and g functions and where f a b and g c d are in normal form, can’t be unified05/12 17:16
pgiarrussoin *that* case, though, you might be able to fix the issue by splitting on a/b/c/d so that the calls to f and g reduce05/12 17:17
pgiarrussooverall, you need to actually think through the formal rules for both unification and normalization (or have intuition of those rules) to debug these issues05/12 17:18
pgiarrussoif the intuition stays semantic, it doesn’t help05/12 17:18
pgiarrusso*sometimes, the more general lemma can be a standard one—cong, subst, trans, ...05/12 17:19
pgiarrussoother times, you need a custom one05/12 17:19
pgiarrussoafraid I don’t have examples ready :-|05/12 17:19

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