--- Day changed Sat Sep 09 2017
WilliamHamiltonhi all, I'm here to ask for some help with equality and existential hiding09/09 11:05
WilliamHamiltonlet's say I have the type09/09 11:05
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-09_10:05:58.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/xokIzEWLstynFrWvLonrPmJx>09/09 11:05
WilliamHamilton(a standard encoding of De Brujin variables)09/09 11:06
WilliamHamiltonI can talk about the "class" of all variables, indipendently of the type on which they're defined, with:09/09 11:06
WilliamHamilton```09/09 11:07
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-09_10:07:14.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/tKFrqdnERcarfvGprRIVIzUr>09/09 11:07
WilliamHamiltonand I can of course translate the concrete representation in the generic one with:09/09 11:07
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-09_10:07:53.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/IOluXlseSPUAIIbKnpLKUEMi>09/09 11:07
WilliamHamiltonnow, I'd like to say that two variables are equal, knowing that they have equal `toAVar`, in this sense:09/09 11:09
* WilliamHamilton sent a long message: WilliamHamilton_2017-09-09_10:09:41.txt <https://matrix.org/_matrix/media/v1/download/matrix.org/TWzKmRMXFepqYCQWECCgDUIt>09/09 11:09
WilliamHamiltonobviously this doesn't compile, because v1 and v2 don't have, a priori, the same type09/09 11:10
WilliamHamiltonbut is there a way to express this idea?09/09 11:10
WilliamHamiltonfor reference, the complete code for this question is at: http://lpaste.net/35831209/09 11:11
WilliamHamiltonthe problem I was trying to solve is unifying two variables once I know that they have the same AVar form, at line http://lpaste.net/358312#line13909/09 11:25
comietek_<_ would probably read better as _,_09/09 11:49
comietekWilliamHamilton: you may be looking for heterogeneous equality09/09 11:50
comietekhttp://agda.github.io/agda-stdlib/Relation.Binary.HeterogeneousEquality.html09/09 11:51
comieteksection 5.1.3, John Major equality, Conor McBride’s thesis, http://strictlypositive.org/thesis.pdf09/09 11:52
WilliamHamiltonI read the description of this equality in the agda stdlib, let me see the thesis though09/09 12:06
WilliamHamilton(the first time, I understood that it's the right idea, but not how to use it)09/09 12:06
apostolisHello . I cannot compile agda with the current default.nix file. It is missing blaze-html and uri-encode dependencies. Is there anyone familiar with the nixos distribution?09/09 20:15
zachkdo you have cabal install working? 09/09 20:16
apostolisI don't know. I install agda by pulling nixpkgs and then adding a custom package like in the guide.09/09 20:18
zachkdoes nix have a haskell-platform package, that comes with cabal install, then you could just do cabal install agda09/09 20:19
apostolisMost probably the dependencies changed but the default.nix file hasn't.09/09 20:19
apostolisSure it has.09/09 20:19
zachkinstall haskell-platform, then just type cabal update ; cabal install agda09/09 20:20
zachkthough I don't think the cabal agda package comes with the agda stdlib09/09 20:20
apostolisI want to compile agda from github.09/09 20:20
apostolisnixos has most packages in isolation, so one would need to set up an environment before calling cabal install. I do not know how to do that.09/09 20:22

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