--- Log opened Fri Feb 23 09:10:53 2018
-!- Irssi: #agda: Total of 123 nicks [0 ops, 0 halfops, 0 voices, 123 normal]23/02 09:10
-!- Irssi: Join to #agda was synced in 134 secs23/02 09:13
mudri[m]pie_: Yes. I think the only necessary exotic Unicode symbol is ‘⊔’ (for levels), if you're happy to not use stdlib.23/02 14:16
mudri[m]And the current master version has some option that makes agda-mode not generate exotic Unicode symbols.23/02 14:17
pie_(asking for a friend)23/02 14:17
pie_thanks23/02 14:17
mudri[m]Conor McBride and his students work in ASCII, so it's to some extent practicable.23/02 14:20
Saizan⊔ is not needed either23/02 15:47
Saizanwell, i guess it is if you import Agda.Primitive23/02 15:48
Saizanwhich at some point you might have to, yeah23/02 15:49
Saizanyou can rename it right away though :)23/02 15:49
dolioJust use induction-recursion to define your own trasnfinite universe hierarchy inside Set.23/02 17:13
taktoado floats from Agda.Builtin.Float have propositional equality (ignoring NaN)?23/02 17:20
taktoaoh I guess they have decidable equality so whatever23/02 17:20
mudri[m]Does anyone use Agda's library system on NixOS? I haven't looked into it, but whatever Nix script it is seems to delete the .agda-lib file from, for example, stdlib.23/02 20:53

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