--- Day changed Sun Feb 26 2017 | ||

wedify | mudri: 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/352985 | 26/02 00:01 |

mudri | wedify: ^ that's where I'm starting from. | 26/02 00:02 |

mudri | Look at the goal and context, and (if I'm inferring the types right in my head), modus ponens should suffice. | 26/02 00:03 |

glguy | wedify: If you have a function: 2==2 -> _|_ and you need a _|_ , then apply your function to refl | 26/02 00:04 |

mudri | Looking at it again, you might get incomplete pattern matching warnings. I'll load it up and have a look... | 26/02 00:06 |

glguy | it works out just fine | 26/02 00:06 |

mudri | There should be some case for noDupSingle somewhere, and Agda seems to agree with me. | 26/02 00:09 |

glguy | Agda checks it alright | 26/02 00:10 |

glguy | af (notMember x x₁) = x refl | 26/02 00:10 |

glguy | and | 26/02 00:10 |

glguy | ae (noDup x (notMember x₁ x₂)) = x₁ refl | 26/02 00:10 |

wedify | ok i got it. thanks guys :) | 26/02 00:11 |

mudri | Apparently 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 |

wedify | yeah i should use it more | 26/02 00:13 |

wedify | used to languages without it :) | 26/02 00:13 |

mudri | I think the trick is that I barely do programming any more. ;-) | 26/02 00:15 |

wedify | how do you mean? you just do math now? | 26/02 00:19 |

mudri | Basically, yeah. I find it easier to do interesting little proofs than interesting little programs. | 26/02 00:30 |

mudri | And I have my dissertation project... | 26/02 00:30 |

wedify | i 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 |

wedify | i have a book coming called 'constructive real analysis'. i have a goal of doing those proofs in agda | 26/02 00:32 |

wedify | i used to hate math but thanks to haskell and agda i'm starting to like it | 26/02 00:33 |

wedify | what's your dissertation? | 26/02 00:34 |

mudri | I (try to) prove correct a weird algorithm for shortest distances in a graph. Dijkstra's algorithm, but more general. | 26/02 00:41 |

mudri | I'll find the paper... | 26/02 00:41 |

mudri | http://www.cs.nyu.edu/~mohri/pub/jalc.pdf | 26/02 00:42 |

mudri | Constructive real analysis sounds interesting, though. Who's it by? | 26/02 00:44 |

wedify | Allen Goldstein | 26/02 00:45 |

mudri | I 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 |

mudri | That 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 secs | 26/02 05:29 | |

lpaste_ | wedify pasted “what do you think?” at http://lpaste.net/352996 | 26/02 05:34 |

wedify | i'm working on my dependently typed chess expressions again | 26/02 05:34 |

wedify | this time around is a lot easier than last time | 26/02 05:34 |

wedify | just jump to the end for the part i'm interested in hearing about | 26/02 05:36 |

wedify | the definitions of the moves | 26/02 05:36 |

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