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

--- Day changed Sat May 06 2017
subttleIs it possible to write catMaybes for Vec using an existential or something similar?06/05 07:15
subttlesomething like06/05 07:15
subttlecatMaybes : ∀ {n : ℕ} {a} {A : Set a} → Vec (Maybe A) n → ∃ (λ m → (Vec A m))06/05 07:15
subttleI tried doing it but I'm not sure I'm on the right path (if it's possible)06/05 07:16
subttleI'm going to paste what I tried because it's only 3 lines06/05 07:17
subttlecatMaybes []             = 0 , []06/05 07:17
subttlecatMaybes (nothing ∷ xs) = catMaybes xs06/05 07:17
subttlecatMaybes (just  x ∷ xs) = (ℕ.suc ?) , (x ∷ ?)06/05 07:17
subttleI saw something similar done in I think Idris, using an existential in the signature for filter on Vec06/05 07:20
subttlehm, I should probably use ∃! now that I think about it :D06/05 07:26
subttleAlso, one related question. Is it possible to extract the implicit length of xs on the LHS? How would I do that? Thanks in advance!!06/05 07:28
subttleha, okay looking for that Idris example to make sure I was remembering that correctly and I think I found what I need, actually! https://github.com/idris-lang/Idris-dev/blob/0d3d2d66796b172e9933360aee51993a4abc624d/libs/base/Data/Vect.idr#L49706/05 07:39
subttlejust in case anyone cares, I ended up with06/05 07:51
subttlecatMaybes (just  x ∷ xs) = let (m , ys) = catMaybes xs in (ℕ.suc m) , x ∷ ys06/05 07:51
subttlenow I'm going to try and rewrite it to the there-exists-unique version :)06/05 07:52
mudriI'm having some problems with indentation in the LaTeX backend. Specifically, in a data declaration where “data” and “where” are on different lines, the constructors don't get indented.06/05 15:04
mudriMinimal example:06/05 15:04
lpastemudri pasted “No title” at http://lpaste.net/35527206/05 15:04

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