--- Day changed Sun Mar 26 2017
mietekhow can I get Agda to search for instances within a pair?26/03 03:16
mietekuniq∈ {{x≢y , x∥Γ}} (pop i) (pop i′) = cong pop (uniq∈ {{x∥Γ}} i i′)26/03 03:16
mietekthis is what I have to write now26/03 03:16
mietekmanually unpack the instance and pass the right projection26/03 03:16
mietekI thought declaring the _,_ constructor as instance would be enough, but no26/03 03:17
mietekhm, maybe there’s more than one in scope26/03 03:35
vorgangHello. When I start emacs mode with C-c C-l, I get an error "The Agda mode's version (2.5.2) does not match that of agda (". Wiping cabal and reinstalling Agda won't help; I've done that twice already. Please help.26/03 19:44
wedifyvorgang: i assume that when you run 'agda --version' it gives ''? where does 'which agda' say it's coming from?26/03 22:35

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