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

--- Day changed Sun Mar 12 2017
structuralistI'm having a hard time finding documentation for sized types -- can anyone explain what this is (how is Size different from Nat) and how to use it?12/03 02:11
structuralistThe manual is not very helpful12/03 02:12
structuralistMaybe more concrete question: what's a simple example of something that's accepted with sized types and rejected without?12/03 02:20
structuralist(That is, with --no-sized-types off vs. on)12/03 02:21
akr[m]here's something that wouldn't work without the use of sized types, I don't know about --no-sized-types12/03 08:20
akr[m]http://lpaste.net/35331812/03 08:20
akr[m]ℕ's wouldn't typecheck, because Agda would have no way of knowing that map doesn't do something silly like throw away the first 5 elements and then map12/03 08:21
akr[m]practically, I think Size is ℕ + {ω}12/03 08:22
canndrewanyone have any advice for proving things like (f x y z) ≡ (g a b c) where f and g are dependent functions?12/03 14:01
canndrewI'm trying to use cong and friends but it gets really messy real quick because i keep ending up with things having different (but equal) types12/03 14:03
canndreweg. I can prove that (f = g) and (x = a) but then I can't say that (f x = g a) because they have different types. I also can't prove (y = b) for the same reason12/03 14:06
canndrewah, looks like agda has heterogeneous equality in the stdlib that i could use..12/03 14:26

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