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

--- Day changed Mon Jan 30 2017
rribeiroHello all! I'm with a trouble in a lemma definition type due to problems with levels. The minimum code is at http://lpaste.net/564278629471617024030/01 15:41
rribeiroCould someone take a look and give me a clue?30/01 15:41
glguyrribeiro: did you perhaps intend to write: ∃ instead of Σ 30/01 16:52
rribeiroglguy: But they should be the same, no?30/01 16:53
glguyno30/01 16:53
rribeiroNo? But both are dependent products right?30/01 16:53
glguyrribeiro: ∃ = Σ _30/01 17:25
glguyThey both construct a 'record Σ', but ∃ infers one of the parameters30/01 17:27
glguyhttps://agda.github.io/agda-stdlib/Data.Product.html30/01 17:27
mietekYep30/01 17:43
rribeiroglguy: You're right. It worked, thanks!30/01 18:23

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