--- Day changed Sun Dec 31 2017 | ||

robwebbjr | Hello. Would you please help me with trivial issue? I'm just learning Agda along with discrete math and I simply need to prove that adding two even integers results in an even integer. I'm ok with the proof but I am having a difficult time trying to get Agda to recognize evens from odds. Simple in most any other language... The details are here: http://lpaste.net/360556 I've tried several approaches, the last two are included. Thank | 31/12 00:33 |
---|---|---|

Saizan | robwebbjr: you should use "Data.Fin.zero" rather than Data.Fin.Fin 0 | 31/12 00:41 |

Saizan | robwebbjr: also, maybe you want an inductive definition instead of one based on division | 31/12 00:41 |

robwebbjr | HI! Thank you! I'll try it right now! | 31/12 00:42 |

robwebbjr | OK, wait. I had an inductive definition initially. Is that one fixable. (The one at the bottom?) | 31/12 00:43 |

robwebbjr | So i tried Data.Fin.zero without success... http://lpaste.net/360556 | 31/12 00:46 |

robwebbjr | I realize i left the base case out of the inductive version i pasted, but that was just a copt issue-- i put in now so you can see it. | 31/12 00:50 |

robwebbjr | Hello. I got knocked off line, if you are still around <Saizon> ? Maybe some one else can take a look? I'm simply trying to make an isEven function. Here is what I've tried: http://lpaste.net/360556 | 31/12 01:11 |

mietek | robwebbjr: what do you mean by “the Agda book by Stump jumped into Braun trees”? | 31/12 01:14 |

mietek | robwebbjr: Braun trees are section 5.4 on page 118 | 31/12 01:15 |

robwebbjr | Lol, yeah... Verified Funtional Programming with Agda by Aaron Stump. | 31/12 01:16 |

robwebbjr | yes | 31/12 01:16 |

robwebbjr | I am only a little familiar with trees from the Haskell book | 31/12 01:16 |

mietek | robwebbjr: have you worked through the previous chapters? done the exercises? | 31/12 01:16 |

mietek | you can find an answer to your question in the library Iowa Agda Library | 31/12 01:17 |

robwebbjr | Yes. but i switched to a discrete math text to get some background knowledge | 31/12 01:17 |

mietek | but you’re not asking about discrete math | 31/12 01:18 |

mietek | https://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/1.3/nat.agda | 31/12 01:18 |

robwebbjr | Really? I don't recall that. I will go look right now. | 31/12 01:18 |

mietek | is-even : ℕ → 𝔹 | 31/12 01:18 |

robwebbjr | I was asking because the math text says prove addeing two evens makes an even. I can do the proof if i couls get agda to give me an isEven function | 31/12 01:19 |

mietek | Agda proofs are usually going to be a little different than proofs found in the average mathematics book | 31/12 01:20 |

mietek | my point is, you already have a good book on Agda | 31/12 01:20 |

mietek | on page 69, you can find a definition of `is-even` | 31/12 01:21 |

mietek | (figure 3.9) | 31/12 01:21 |

robwebbjr | Hurray!!! That's right, mutual recursion!!!! | 31/12 01:21 |

robwebbjr | I forgot all about it!! | 31/12 01:22 |

robwebbjr | Thanks so much! | 31/12 01:22 |

mietek | you’re welcome. just… read it :) | 31/12 01:22 |

robwebbjr | So yeah, I'm actually having great fun with the book -- I just had a hard time following the code about the BSTs | 31/12 01:23 |

robwebbjr | The math text is actually helping. I've learned a lot about agda just doing the exercises so far -- like coding digital logic gates | 31/12 01:24 |

robwebbjr | Anyway, thanks again!! | 31/12 01:24 |

fsestini | hi all. I was trying to use do-notation in agda 2.5.3, but I’m getting a ‘not in scope’ error. Are there some imports that I’m missing? | 31/12 15:00 |

{AS} | fsestini: I believe it is available on git master | 31/12 16:32 |

{AS} | not in Agda 2.5.3 | 31/12 16:32 |

fsestini | <{AS}>: oic | 31/12 16:36 |

fsestini | I’ll try to pull it from git then. thanks | 31/12 16:37 |

robwebbjr | Hello. I have a newbie question here: http://lpaste.net/360556 (I am working through Stump's text). Would you please help me? Thank you. | 31/12 20:15 |

mietek | robwebbjr: the error message you get concerns your definition of `zero-matrix` | 31/12 20:21 |

mietek | you wrote `zero-matrix r c = 𝕍 (repeat𝕍 0 c) r` | 31/12 20:21 |

mietek | you wanted to write `zero-matrix r c = repeat𝕍 (repeat𝕍 0 c) r` | 31/12 20:22 |

robwebbjr | Hi again. and yes | 31/12 20:22 |

robwebbjr | really? | 31/12 20:22 |

robwebbjr | i'll go try right now... | 31/12 20:23 |

mietek | read it aloud | 31/12 20:23 |

mietek | first, you define what a `r by c matrix` is: it is a `𝕍 (𝕍 ℕ c) r` | 31/12 20:23 |

mietek | so, a vector with `r` elements, such that every element is a vector of `c` elements | 31/12 20:23 |

robwebbjr | ooohhhh, right! | 31/12 20:24 |

mietek | now, you want to give an inhabitant of the `r by c matrix` type | 31/12 20:24 |

robwebbjr | of course. makes perfect sense, once you point it out... | 31/12 20:24 |

mietek | the error message you got is confusing because it assumes that you really did want to use `𝕍` and it’s the argument that is wrong | 31/12 20:25 |

mietek | but the argument is correct | 31/12 20:25 |

robwebbjr | thank you so much for your friendly help . I find myself missing the forest for the trees with agda | 31/12 20:26 |

mietek | you’re welcome | 31/12 20:26 |

robwebbjr | happy new year!! | 31/12 20:26 |

mietek | happy new year :) | 31/12 20:26 |

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