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

--- Day changed Tue Feb 27 2018
mbrockwhoo, I'm using I/O via Haskell. I'm a bit confused about how I can, let's say, turn a `String` I get from I/O into either a `Vec Char 10` or nothing27/02 21:23
mbrockwell, I did come up with a way that involves the pattern `x1 :: x2 :: ... :: x20 :: []`27/02 21:29
mudri[m]mbrock: It probably works out nicely if you write a more general function of type (n : ℕ) → List A → Maybe (Vec A n) by induction on n.27/02 22:15
mbrockmudri[m]: aha! thanks, I'll try that27/02 22:15

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