--- Day changed Sun Feb 26 2017
wedifymudri: could you clarify? i can give  '2 ≡ 2 → ⊥' refl for an argument but then i have no way to construct a ⊥26/02 00:00
lpaste_mudri revised “stuck on af”: “stuck on af” at http://lpaste.net/35298526/02 00:01
mudriwedify: ^ that's where I'm starting from.26/02 00:02
mudriLook at the goal and context, and (if I'm inferring the types right in my head), modus ponens should suffice.26/02 00:03
glguywedify: If you have a function:   2==2 -> _|_   and you need a  _|_ , then apply your function to refl26/02 00:04
mudriLooking at it again, you might get incomplete pattern matching warnings. I'll load it up and have a look...26/02 00:06
glguyit works out just fine26/02 00:06
mudriThere should be some case for noDupSingle somewhere, and Agda seems to agree with me.26/02 00:09
glguyAgda checks it alright26/02 00:10
glguyaf (notMember x x₁) = x refl26/02 00:10
glguyand 26/02 00:10
glguyae (noDup x (notMember x₁ x₂)) = x₁ refl26/02 00:10
wedifyok i got it. thanks guys :)26/02 00:11
mudriApparently I use agda-mode's case splitting more than other people (i.e, pretty much always). It seems to work out okay, though.26/02 00:12
wedifyyeah i should use it more26/02 00:13
wedifyused to languages without it :)26/02 00:13
mudriI think the trick is that I barely do programming any more. ;-)26/02 00:15
wedifyhow do you mean? you just do math now?26/02 00:19
mudriBasically, yeah. I find it easier to do interesting little proofs than interesting little programs.26/02 00:30
mudriAnd I have my dissertation project...26/02 00:30
wedifyi started learning agda because i wanted to express stronger types for my programs and now it's getting me into the math side of things :)26/02 00:32
wedifyi have a book coming called 'constructive real analysis'. i have a goal of doing those proofs in agda26/02 00:32
wedifyi used to hate math but thanks to haskell and agda i'm starting to like it26/02 00:33
wedifywhat's your dissertation?26/02 00:34
mudriI (try to) prove correct a weird algorithm for shortest distances in a graph. Dijkstra's algorithm, but more general.26/02 00:41
mudriI'll find the paper...26/02 00:41
mudrihttp://www.cs.nyu.edu/~mohri/pub/jalc.pdf26/02 00:42
mudriConstructive real analysis sounds interesting, though. Who's it by?26/02 00:44
wedifyAllen Goldstein26/02 00:45
mudriI don't understand the Amazon blurb, so I can't say much more. :-/26/02 00:49
mudri“This book is concerned with processes for finding roots of functions.”26/02 00:54
mudriThat seems an odd introduction.26/02 00:54
--- Log closed Sun Feb 26 05:27:02 2017
--- Log opened Sun Feb 26 05:27:10 2017
-!- Irssi: #agda: Total of 118 nicks [0 ops, 0 halfops, 0 voices, 118 normal]26/02 05:27
-!- Irssi: Join to #agda was synced in 134 secs26/02 05:29
lpaste_wedify pasted “what do you think?” at http://lpaste.net/35299626/02 05:34
wedifyi'm working on my dependently typed chess expressions again26/02 05:34
wedifythis time around is a lot easier than last time26/02 05:34
wedifyjust jump to the end for the part i'm interested in hearing about26/02 05:36
wedifythe definitions of the moves26/02 05:36

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