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

--- Day changed Sun Apr 30 2017
TanebHow would I do something like "fibs = 0 : 1 : zipWith (+) fibs (tail fibs)" in Agda?30/04 12:04
comietekTaneb: musical notation or copattern notation30/04 12:13
TanebI'm trying that, with "fibs = 0 :: # (1 :: zipWith _+_ fibs (tail fibs))" (plus Unicode) I'm getting "Termination checking failed for the following functions: fibs"30/04 12:15
comietekwhat is the type of fibs?30/04 12:20
TanebNat30/04 12:20
TanebStream Nat, rather30/04 12:20
comietekI'll give it a go on a bit30/04 12:21
comietekin*30/04 12:21
Taneb:)30/04 12:21
comieteksee if you can use an explicit unfold instead30/04 12:21
akr[m]Taneb: firstly I think you need to use sized types30/04 13:42
akr[m]see e.g. https://lists.chalmers.se/pipermail/agda/2017/009352.html30/04 13:42
subttleHi, I have a question regarding Record module syntax... I'm looking here: http://agda.readthedocs.io/en/latest/language/record-types.html#record-modules and I don't think I see exactly what I need, so I'm asking here... is it possible to define a function in the record module scope that returns a modified version of itself... I know if the _field_ were to do that then the record would be recursive and I 30/04 19:35
subttlewould need induction/coinduction, but30/04 19:36
subttleif I were to just use the Functor code on that page as an example30/04 19:36
subttleI want to define a function in the same scope as _<$_30/04 19:36
subttlebut returns an instance of Functor30/04 19:36
subttle(I'm not working with Functors, I have a different record)30/04 19:37
subttlei.e. I want to add an arbitrary definition to the record module, but the return type is that of the record itself30/04 19:38
subttlehopefully I said that correctly :D30/04 19:38
subttleMore concretely, I have a DFA record I'm working on which has three fields (q0, delta, F), and I want to define a function which returns the right-language with respect to some state, q30/04 19:41
subttleand to do that, I just take the current DFA and set q0 to the new state q30/04 19:41
subttleI defined the function just fine outside the scope of the record module30/04 19:42
subttleright : ∀ {∣Q∣ ∣Σ∣ : ℕ} {Q : Fin ∣Q∣} {Σ : Fin ∣Σ∣} → DFA Q Σ → Fin′ Q → DFA Q Σ30/04 19:42
subttleright m q = record { DFA m ; q₀ = q }30/04 19:42
subttlebut I would like to move that code into the record module scope and I'm getting yellow highlights every way I try30/04 19:43
subttleinside the scope would just be something like:30/04 19:44
subttleright : Fin′ Q → DFA Q Σ30/04 19:44
subttleright q = ?30/04 19:44
subttleOr does the note under http://agda.readthedocs.io/en/latest/language/record-types.html#record-modules apply to my question and mean I can't do it?30/04 19:53
subttleMy constructor, `dfa` is not in scope, but I was hoping some record update syntax would allow it30/04 19:56
subttleand I want to define a function which returns the 30/04 20:05
subttleDFA which produces the right-language of the current DFA/ is what I meant to say :D30/04 20:07

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