--- Day changed Sun Dec 31 2017
robwebbjrHello. 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. Thank31/12 00:33
Saizanrobwebbjr: you should use "Data.Fin.zero" rather than Data.Fin.Fin 031/12 00:41
Saizanrobwebbjr: also, maybe you want an inductive definition instead of one based on division31/12 00:41
robwebbjrHI! Thank you! I'll try it right now!31/12 00:42
robwebbjrOK, wait. I had an inductive definition initially. Is that one fixable. (The one at the bottom?)31/12 00:43
robwebbjrSo i tried Data.Fin.zero without success... http://lpaste.net/36055631/12 00:46
robwebbjrI 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
robwebbjrHello. 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/36055631/12 01:11
mietekrobwebbjr: what do you mean by “the Agda book by Stump jumped into Braun trees”?31/12 01:14
mietekrobwebbjr: Braun trees are section 5.4 on page 11831/12 01:15
robwebbjrLol, yeah... Verified Funtional Programming with Agda by Aaron Stump. 31/12 01:16
robwebbjryes31/12 01:16
robwebbjrI am only a little familiar with trees from the Haskell book31/12 01:16
mietekrobwebbjr: have you worked through the previous chapters? done the exercises?31/12 01:16
mietekyou can find an answer to your question in the library Iowa Agda Library31/12 01:17
robwebbjrYes. but i switched to a discrete math text to get some background knowledge31/12 01:17
mietekbut you’re not asking about discrete math31/12 01:18
mietekhttps://svn.divms.uiowa.edu/repos/clc/projects/agda/ial-releases/1.3/nat.agda31/12 01:18
robwebbjrReally? I don't recall that. I will go look right now.31/12 01:18
mietekis-even : ℕ → 𝔹31/12 01:18
robwebbjrI 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 function31/12 01:19
mietekAgda proofs are usually going to be a little different than proofs found in the average mathematics book31/12 01:20
mietekmy point is, you already have a good book on Agda31/12 01:20
mietekon page 69, you can find a definition of `is-even`31/12 01:21
mietek(figure 3.9)31/12 01:21
robwebbjrHurray!!! That's right, mutual recursion!!!!31/12 01:21
robwebbjrI forgot all about it!!31/12 01:22
robwebbjrThanks so much!31/12 01:22
mietekyou’re welcome. just… read it :)31/12 01:22
robwebbjrSo yeah, I'm actually having great fun with the book -- I just had a hard time following the code about the BSTs31/12 01:23
robwebbjrThe math text is actually helping. I've learned a lot about agda just doing the exercises so far -- like coding digital logic gates31/12 01:24
robwebbjrAnyway, thanks again!!31/12 01:24
fsestinihi 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 master31/12 16:32
{AS}not in Agda 2.5.331/12 16:32
fsestini<{AS}>: oic31/12 16:36
fsestiniI’ll try to pull it from git then. thanks31/12 16:37
robwebbjrHello. 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
mietekrobwebbjr: the error message you get concerns your definition of `zero-matrix`31/12 20:21
mietekyou wrote `zero-matrix r c = 𝕍 (repeat𝕍 0 c) r`31/12 20:21
mietekyou wanted to write `zero-matrix r c = repeat𝕍 (repeat𝕍 0 c) r`31/12 20:22
robwebbjrHi again. and yes31/12 20:22
robwebbjrreally?31/12 20:22
robwebbjri'll go try right now...31/12 20:23
mietekread it aloud31/12 20:23
mietekfirst, you define what a `r by c matrix` is: it is a `𝕍 (𝕍 ℕ c) r`31/12 20:23
mietekso, a vector with `r` elements, such that every element is a vector of `c` elements31/12 20:23
robwebbjrooohhhh, right!31/12 20:24
mieteknow, you want to give an inhabitant of the `r by c matrix` type31/12 20:24
robwebbjrof course. makes perfect sense, once you point it out...31/12 20:24
mietekthe error message you got is confusing because it assumes that you really did want to use `𝕍` and it’s the argument that is wrong31/12 20:25
mietekbut the argument is correct31/12 20:25
robwebbjrthank you so much for your friendly help . I find myself missing the forest for the trees with agda31/12 20:26
mietekyou’re welcome31/12 20:26
robwebbjrhappy new year!!31/12 20:26
mietekhappy new year :)31/12 20:26

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