--- Day changed Sun Apr 09 2017
subttleHi, I have a question about proving something about a list fold. The foldr₁ in question is over a small, fixed, non-empty list. Essentially something like this:09/04 00:51
subttlefoldr₁ (λ x accum → <whatever>) (a NE.∷ b ∷ c ∷ d)09/04 00:51
subttleThe end goal is:09/04 00:51
subttle∣x∣ + ∣accum∣ ≤ ∣a∣ + ∣b∣ + suc (∣c∣ + ∣d∣)09/04 00:52
subttlewhere ∣x∣ is (size x), etc.09/04 00:52
subttleI can think of a few ways to approach this, one being I can say that x can only ever be one of those four elements, etc. But I feel like there is probably a more elegant (and less tedious) approach...09/04 00:52
subttlePerhaps using https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Properties.agda09/04 00:52
subttleAnyone care to enlighten me? It would be appreciated. Thank you.09/04 00:52
subttlePlease let me know if I have not given enough information :)09/04 00:59
canndrew_mietek: thanks, i've switched to putting everything inside a mutual block and now i can get a little bit further.09/04 15:29
canndrew_{AS}: thanks, i've tring spacemacs now. It's very similar to the vim agda mode except it display slightly more useful information09/04 15:31
canndrew_when agda gives me a type error and the type error contains a bunch of variables that it made up, how can i get it to tell me what those variables mean?09/04 15:32
gallaiscanndrew_: you can start explicitly introducing implicit variables09/04 16:14
mudriHas anyone found a good way to mix literate Agda and literate Haskell in a single LaTeX document?09/04 16:22
canndrew_gallais: thanks, that't what i do. it doens't always work though.09/04 16:39
canndrew_is there a command to increase the verbosity of the errors from inside emacs?09/04 16:39
{AS}canndrew_: np. I am unsure about verbosity though09/04 17:04
mietekcanndrew_: have you tried "Show Hidden"?09/04 19:25
mietekC-c C-x C-hToggle display of hidden arguments09/04 19:25
mietekit sticks until the next load09/04 19:26
mietekthe results are usually unreadable, but sometimes help09/04 19:26
gallaiscanndrew_: if you want to see debug info, you can add a pragma at the top of your file09/04 19:44
gallais{-# OPTIONS -vtopic.subtopic:level #-}09/04 19:44
gallaisand then the info will show up in the debug buffer09/04 19:44
gallaisThese topic/subtopic are not listed anywhere though. The easiest way to find them is to grep Agda's sources for "reportSDoc" and "reportSLn" and then find something that looks like what you're interested in09/04 19:46
gallaislevels are (more or less) increments of 10 from 0 to 10009/04 19:47

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