/home/laney/.irssi/irclogs/Freenode/#agda.log-20180116

--- Day changed Mon Jan 15 2018
Guest57308Текст ниже запросил awesomelackware.15/01 09:48
Guest57308ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ!15/01 09:48
Guest57308ГОВНО ТЫ15/01 09:48
Guest57308САМ ТЫ ШИЗИК!15/01 09:48
Guest57308ИДИ ДАЛЬШЕ15/01 09:48
Guest57308ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ!15/01 09:48
Guest57308ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ!15/01 09:48
Guest57308САМ ТЫ ШИЗИК!15/01 09:48
Guest57308ЗАКРОЙ РОТ15/01 09:48
Guest57308ЗАКРОЙ РОТ15/01 09:48
Guest57308Я НЕ ШИЗИК15/01 09:48
Guest49588Текст ниже запросил awesomelackware.15/01 09:49
Guest49588Я НЕ ШИЗИК15/01 09:49
Guest49588ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ!15/01 09:49
Guest49588ГОВНО ТЫ15/01 09:49
Guest49588ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ!15/01 09:49
Guest49588ИДИ ДАЛЬШЕ15/01 09:49
Guest49588САМ ТЫ ШИЗИК!15/01 09:49
Guest49588Я НЕ ШИЗИК15/01 09:49
Guest49588ГОВНО ТЫ15/01 09:49
Guest49588ССУ ТЕБЕ В ЛИЧКУ!15/01 09:49
Guest49588ГОВНО ТЫ15/01 09:49
Bratishkaawesomelackware: заебал, не сри здесь, дебил.15/01 09:49
awesomelackwareBratishka, иди нахуй15/01 09:49
BratishkaSorry guys, He is just stupid F#-lover15/01 09:49
awesomelackwareSorry guys15/01 09:49
awesomelackwareBratishka is stupid Scala user15/01 09:49
awesomelackwareF# > Scala15/01 09:54
awesomelackwarejfdm, 卐15/01 10:40
awesomelackwaretwanvl, ты хуй15/01 10:54
awesomelackwareбля15/01 10:54
awesomelackwareГЕИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareШИЗИКИ15/01 10:54
awesomelackwareГЕИ15/01 10:54
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareГЕИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:55
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareШИЗИКИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:56
awesomelackwareГЕИ15/01 10:57
awesomelackwareГЕИ15/01 10:57
awesomelackwareШИЗИКИ15/01 10:57
awesomelackwareГЕИ15/01 10:57
awesomelackwareГЕИ15/01 10:57
awesomelackwareГЕИ15/01 10:57
awesomelackwareГЕИ15/01 10:57
awesomelackwareШИЗИКИ15/01 10:57
awesomelackwareШИЗИКИ15/01 10:57
m0rphism weird bots o.0'15/01 11:35
pgiarrussojust learned that `/msg ChanServ access #agda list` gives the list of ops of this channel and we just got a new one15/01 14:21
Nik05are you pgiarrusso ?15/01 14:29
Nik05oh mietek is15/01 14:30
Nik05pgiarrusso im trying to define a relational type in which inhabitants need to be a subset of A <x> B, is this possible?15/01 14:37
pgiarrussoNik05: in type theory it’s easier to encode subsets of S as predicates on members of S (S -> Set), but I think we discussed this?15/01 14:48
Nik05yes15/01 14:48
pgiarrussois A <x> B a typo for not (A == B)15/01 14:48
pgiarrusso?15/01 14:49
Nik05<x> is the set cross product from Relation.Unary15/01 14:49
pgiarrussoI’m also not sure on “relational type” and “inhabitants need to be subset”, but are you trying to write `data Foo : Set 1 where Bar : (A <x> B -> Set) -> Foo` or something such?15/01 14:50
pgiarrussoimportant bit is that predicates at `Set l` can only be contained in types at `Set (suc l)`15/01 14:51
pgiarrussoNik05: ^^15/01 14:51
Nik05let me try to explain what i meant15/01 14:52
Nik05Definition 4.2.1. Suppose A and B are sets. Then a set R ⊆ A × B is called a15/01 14:54
Nik05relation from A to B.15/01 14:54
Nik05This is a definition from a book15/01 14:54
pgiarrussoNik05: (0) the Agda standard library defines what is a relation in Agda, and that’s essentially a binary predicate15/01 14:55
pgiarrussoso a relation on A and B is just a member of type `A -> B -> Set`15/01 14:55
Nik05ok15/01 14:55
pgiarrusso(1) but you’re correctly noticing that does *not* model the book definition15/01 14:56
pgiarrussoindeed, that book is giving a standard set-theoretic definition, and some set-theoretic concepts need to be modified to be expressed in type theory15/01 14:56
pgiarrussoand this is just another example15/01 14:57
pgiarrussoOTOH, if you want, you can use time `A \times B -> Set`, it’s equivalent to `A -> B -> Set` by currying, but as a matter of style often the latter is preferred15/01 14:58
Nik05SO this would be a correct definition: R = Pred A l1 \to Pred B l2 \to Set _?15/01 14:58
Nik05where A and B are the predicate variables15/01 14:59
pgiarrussoNik05: no, you want `R = A -> B -> Set l`, or `R = A \times B -> Set l`, or `R = Pred (A \times B) l` — they’re all equivalent15/01 15:40
Nik05but then my set isnt a subset of the crossproduct of the two other sets15/01 15:46
Nik05how do i make my predicate depend on the two other predicates?15/01 15:47
Nik05lets say i got the predicate Four = _<_ 4 : Pred Nat zero15/01 15:49
Nik05Now I want a relation between Four and Four, which should be a subset of Four <x> Four15/01 15:49
Nik05Pred (Nat x Nat) zero is too large, because it can also contain (4, 4)15/01 15:50
Nik05But I guess this isnt possible?15/01 15:52
Nik05Or I need to use a record of which one field is a Pred (Nat x Nat) zero and the other field a proof that that predicate is a subset of Four <x> Four. But then I dont have a set anymore 15/01 15:53
akrHello. `do` notation is first in Agda 2.6, right?15/01 16:50
akrthe official one, anyway https://agda.readthedocs.io/en/latest/language/syntactic-sugar.html15/01 16:58
cartermietek: pgiarrusso  i think the folks at #freenode-sigyn have a spam police bot you can get added to a channel15/01 17:15
Nik05akr agda 2.5.415/01 17:28
Nik05there is not agda 2.615/01 17:28
akroh, hmm15/01 17:29
akrany idea when Arch Linux might get 2.5.4?15/01 17:30
akrNik05: ^15/01 17:30
Nik05sorry i dont know anything about agda (releases), or Arch15/01 17:31
akrnevermind, thanks for clearing up that confusion for me anyway15/01 17:31
akr(website says Agda 2.6.0 and doesn't mention 2.5.4)15/01 17:32
akrugh, why is there in the stdlib `toNat : Char → ℕ` but not `fromNat` is missing?15/01 17:33
akrit is missing, I mean15/01 17:33
pgiarrusso2.6.0 is the codename for master15/01 17:34
pgiarrussoas a rule of thumb, if the stdlib looks incomplete it usually is15/01 17:34
akrso what can be done about this15/01 17:35
akrfromNat needs to be exported from Agda.Builtin.Char or something15/01 17:35
pgiarrussoat least the Agda stdlib, and if you have looked a bit 15/01 17:35
pgiarrussowell, send a PR :-)15/01 17:36
akri mean, primFromNat needs to be exported from there15/01 17:36
pgiarrussoand/or file an issue15/01 17:36
akrhmm, I don't really know about this prim / built-in stuff15/01 17:36
pgiarrussosounds like you're halfway to a fix or at least a good PR15/01 17:36
akrcan I also remove unnecessary imports? :P15/01 17:37
pgiarrussoif you're saying that you need a new primitive and a patch to Agda, well, that's maybe trickier15/01 17:38
pgiarrussobut same thing15/01 17:38
pgiarrussoI mean, Agda devs are busy people and aren't paid to maintain it for everybody's needs, but they do welcome help and are nice15/01 17:39
akroh, wait15/01 17:39
akrprimNatToChar is actually exported from Agda.Builtin.Char15/01 17:39
akrit's just not re-exported by Data.Char15/01 17:39
pgiarrussoOK, so can you do the PR?15/01 17:40
akr(how do you find out what is exported from a module, anyway)15/01 17:40
akryeah15/01 17:40
akrif I can manage to clone the repo on train wifi :P15/01 17:40
pgiarrussootherwise do a edit through GitHub 15/01 17:40
pgiarrussoif you can test the change locally it's nicer though, but might save the cloning :-)15/01 17:41
akr"do a edit through GitHub" … and not have my code type-checked? you must be crazy :P15/01 17:42
pgiarrussoyou have a local copy of the stdlib, no? test it there15/01 17:42
pgiarrussoor do a shallow clone15/01 17:42
akrok, fair point15/01 17:43
pgiarrussobut yes there are trade-offs, and I forget how much CI the stdlib has15/01 17:43
pgiarrussoI think we do have Travis15/01 17:43
pgiarrussoanyway gotta go, but feel free to tag me too in the PR if you do, I'm @blaisorblade15/01 17:43
akrsure thing15/01 17:44
pgiarrussobusy, but if the PR is easy enough I could probably approve it15/01 17:44
akrthanks for the help :)15/01 17:44
pgiarrussoimport cleanups should be separate15/01 17:44
pgiarrussooh wait, not sure I can commit to the stdlib, but maybe I can still offer a review15/01 17:44
pgiarrussowell, thank you for the PR15/01 17:45
pgiarrussobeware I'm on a phone and I haven't checked the code myself though15/01 17:45
pgiarrussobbl15/01 17:45
pgiarrussoakr: ^^15/01 17:46
akrI don't know how to make spacemacs ignore my system-wide installation of stdlib :(15/01 17:51
mietekakr: why do you think it’s a spacemacs thing?15/01 17:51
mietekakr: what’s in your ~/.agda?15/01 17:52
akrwell it's just that as a spacemacs user, I don't really know how emacs works :P thought I should mention that15/01 17:52
pgiarrussoakr: either drop the stdlib from ~/.agda/defaults (or such)15/01 17:52
pgiarrussoor maybe you used the old setup in the emacs config, but that was something you had to do by hand15/01 17:52
pgiarrussoif the 2nd case is false, spacemacs is not involved15/01 17:53
akryeah that's the weird thing, I only have .agda/libraries15/01 17:53
akrand it doesn't have the stdlib15/01 17:53
mietekakr: what’s in your ~/.emacs?15/01 17:53
akryou don't have that with spacemacs15/01 17:53
akrI think it's the doing of the agda spacemacs layer15/01 17:54
mietekbeyond my pay grade15/01 17:55
mietekanyway, next time there’s spam in the channel, ping comietek15/01 17:55
akrhmm, maybe not15/01 17:55
pgiarrussoakr: maybe review customize-group agda-mode? or `~/.spacemacs` ?15/01 17:57
akralready checked .spacemacs, will try the other thing15/01 17:58
pgiarrussoakr: actually, I’d use `ps` to check the command line args agda got15/01 18:00
pgiarrussoakr: if it got any, they come from `SPC SPC customize-group Agda2` (sorry for the imprecision earlier)15/01 18:01
pgiarrussoOTOH, for this patch it might be faster to reinvoke typechecking from the command line, even though it’s not an ideal workflow15/01 18:01
akrhmm ok the include path doesn't come from customize-group15/01 18:03
akrI'm guessing this must be an arch-specific thing15/01 18:06
akrhmm, even if I force it to look elsewhere with `agda --include /dev/null Data/Char/Base.agda` it's still finding my system installation of the stdlib15/01 18:11
akr--no-libraries doesn't help either15/01 18:11
akrweird15/01 18:11
mietektest with plain emacs?15/01 18:13
mietekget rid of your system installation of stdlib?  it’s just a git checkout anyway15/01 18:13
akrthis was running `/usr/bin/agda` from the command line15/01 18:13
mietekhow are you determining that the stdlib is available?15/01 18:13
akrthe include path remains and messes stuff up15/01 18:13
akrwhat do you mean?15/01 18:14
mietekuh.  you’re running agda from the command-line and the include path remains?15/01 18:14
akryeah :/15/01 18:14
mietekhow can you tell?15/01 18:14
akrwell, I still get the same error15/01 18:15
mietekwhich is what?15/01 18:15
akrhttp://lpaste.net/36166515/01 18:15
mietekwhat is the pwd?15/01 18:16
mietekcwd*15/01 18:16
akr/home/osense/dev/agda-stdlib/src15/01 18:17
mietekwhat happens when you just do `agda Data/Char/Base.agda`?15/01 18:17
akrthen it complains about an ambiguous module name, saying it could be referring either to the system installation of the stdlib or my fork in /home15/01 18:18
akrI should've just edited my installation of stdlib in-place15/01 18:19
akrstuff is weird15/01 18:19
mietekwhat happens when you do `agda --no-default-libraries Data/Char/Base.agda`?15/01 18:19
akrsame as one before15/01 18:20
pgiarrussoakr wait no, you might want `—include .`15/01 18:24
pgiarrussoakr that error is not saying that agda knows about the *stdlib*, it says it knows about the *primitive lib*, which it MUST do15/01 18:24
pgiarrussoI don’t know the official name for what I just called “primitive lib”15/01 18:24
pgiarrussobut recent Agdas install a set of .agda files in some “prim” folder and they’re always available (and in fact, required)15/01 18:25
pgiarrussothat’s where the Agda.Builtin.* modules come from15/01 18:25
akrI tried that as well, no luck :| but nevermind, I just edited my system installation of the stdlib and had that type-checked15/01 18:27
pgiarrussoOK good15/01 18:27
pgiarrussomeanwhile, I’m also seeing strange stuff15/01 18:28
akrhmm15/01 18:28
akrmy entire stdlib is in the prim folder15/01 18:28
akrI guess that would explain it15/01 18:29
pgiarrussowat15/01 18:29
pgiarrussowell yeah that sounds broken15/01 18:29
akrI guess the package maintainer thought it would be a good idea :D15/01 18:29
pgiarrussowell... actually... it could even be15/01 18:29
pgiarrussoI mean, for the users who *don’t* modify the stdlib, it does simplify the setup15/01 18:30
pgiarrussobecause users don’t need to put stuff in their `~/.agda`15/01 18:31
akryou don't need to deal with setting it up as a library in your ~/.agda15/01 18:31
akrit does have some advantages15/01 18:31
pgiarrussoakr: OK, we converged :-)15/01 18:31
pgiarrussobut yeah15/01 18:31
akryeah15/01 18:31
pgiarrussoTL;DR. it’s non-standard but works15/01 18:32
akrheh, I'm having a pretty bad delay in my irc client right now15/01 18:32
pgiarrussoah15/01 18:32
pgiarrussowhile for most Haskell packages, the Arch setup is non-standard and *doesn’t* work15/01 18:32
pgiarrussoI don’t use Arch but I’ve seen multiple reports in various forums15/01 18:32
pgiarrussoOTOH, the last interaction we on the Stack side had with the Arch maintainer was helpful — we got them to change something (I forget what)15/01 18:33
akrI heard that nix is good for dealing with haskell packages15/01 18:34
akrhaven't really tried it myself, though15/01 18:35
pgiarrussoI’ve heard it is good and has a steep learning curve15/01 18:38
akrI'm going to add all the other stuff into Data.Char.Base that's exported from Builtin.Char, how should I deal with  `primCharEquality : Char → Char → Bool` ? Should I just re-export it verbatim?15/01 18:39
pgiarrussoand I’m busy enough finishing my PhD :-)15/01 18:39
pgiarrussoakr: uh, not sure there15/01 18:39
akrshould I try to do something with Decidable?15/01 18:40
pgiarrussoit’d be nice to have actual decidable equality, which is non-trivial to get from that primitive :-|15/01 18:40
akrI've only seen it used on Agda-defined datatypes15/01 18:40
mietekno?15/01 18:40
pgiarrussowait15/01 18:40
pgiarrussowait wait15/01 18:40
pgiarrussohave you looked at Data.Char in 0.14?15/01 18:41
pgiarrussoI see a definition of decidable equality15/01 18:41
comietekhttps://www.irccloud.com/pastebin/NYnrRS7L/15/01 18:42
pgiarrussocomietek: Data.Char has something similar15/01 18:43
pgiarrussojust confused because those postulates will make evaluation stuck15/01 18:44
akrah cool15/01 18:44
mietekthis definition worked for me when I was doing names in contexts15/01 18:45
mietekbut it’s probably not ideal15/01 18:45
pgiarrussomietek: s/similar/alpha-equivalent15/01 18:46
pgiarrussomaybe you took Data.Char as inspiration and forgot15/01 18:46
pgiarrussoakr: seems fromNat is still missing15/01 18:46
pgiarrussos/still/indeed/15/01 18:47
akryeah and a bunch of other stuff from Builtin15/01 18:47
pgiarrussoakr: still no clue, but you might want to look into git logs for those files to see if those have a reason for the missing primitives15/01 18:51
pgiarrussomaybe Builtin was updated and the library wasn’t updated yet15/01 18:51
pgiarrusso(which logs would also tell)15/01 18:51
akrthere's even an import for Bool, which you'd need to the other prim functions which are missing15/01 18:51
pgiarrussonot sure if a PR is faster15/01 18:51
akrhmm ok I broke my installation of emacs15/01 18:52
pgiarrussobut looking at logs, while slower, lets you give a superior result15/01 18:52
Nik05`> and I’m busy enough finishing my PhD :-)15/01 18:52
Nik05`Good luck!15/01 18:52
pgiarrussodid you break it through changes to emacs or through changes to the prim folder?15/01 18:52
lambdabot <hint>:1:6: error: lexical error at character 'm'15/01 18:52
pgiarrussodamn it lambdabot, we’re not talking to you just quoting stuff15/01 18:53
pgiarrussoI thought that error was the one from akr’s before I looked at the nick O_O’15/01 18:53
pgiarrussoOK, time to log off and/or sleep and/or study15/01 18:54
Nik05`Oh thats a reply to me15/01 18:54
pgiarrussoyep, but happens to me too, all the time15/01 18:54
pgiarrussoO_O’’’  😓😅15/01 18:54
akrpgiarrusso: changes to the prim folder, which I subsequently erased15/01 18:54
pgiarrussoNik05`: anyway thanks15/01 18:54
akr/usr/share/agda/lib/prim/Data/Char/Core.agdai: openBinaryFile: permission denied (Permission denied)15/01 18:55
Nik05`Have a voor evening15/01 18:55
Nik05`Good*15/01 18:55
pgiarrussoakr: did you edit it as root and have a restrictive umask?15/01 18:55
akrno clue why it's trying to open that file15/01 18:55
akroh well15/01 18:55
pgiarrussoI mean, it does say permission denied15/01 18:55
pgiarrussowell, when it typechecks it tries to write that file15/01 18:55
akrhmm, well I did edit it as root15/01 18:55
pgiarrussounless it’s already up-to-date15/01 18:55
akrhmm15/01 18:56
pgiarrussoOK, retypecheck the changed files as root to restore order15/01 18:56
pgiarrussoand check their permissions are right15/01 18:56
akrbut it doesn't do that when you're just loading that file, I think15/01 18:56
pgiarrusso644 I guess15/01 18:56
akrI mean, no other files in the stdlib have an .agdai with them15/01 18:56
akrI'm just trying to import Data.Char from my project now15/01 18:57
pgiarrussoakr: was that so earlier?15/01 18:57
akrno :)15/01 18:57
pgiarrussoI’d expect all stdlib files to come with their `.agdai`15/01 18:58
pgiarrussobut reinstalling the Arch package is safer than reverse-engineering it15/01 18:59
pgiarrussoakr: just confirmed that my prim folder has an agdai file for each agda one, though it’s not using an Arch package — it’s just an Agda installed through stack15/01 19:00
akroh yeah reinstall fixed it15/01 19:02
akrthanks :)15/01 19:02
-!- mode/#agda [+o mietek] by ChanServ15/01 23:45
-!- mode/#agda [-o mietek] by mietek15/01 23:46

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