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

--- Day changed Wed Mar 22 2017
MathUserCan someone please verify my proof? http://mathb.in/134943 if it is good, I have a follow up question for it (I know it's math related but also know you guys like proofs. I am studying this for type theory)22/03 02:17
apostolisIf the input of a function is known at compile time (constant), will it be replaced by its result when it is compiled? 22/03 04:20
akr[m]https://gist.github.com/osense/ec9b4740e025a70c9e87c35be99b592a22/03 21:51
akr[m]any ideas?22/03 21:51
akr[m]it seems like I should use the existence of omega somehow22/03 22:10
akr[m]I've got a lemma that A ≡ B → A → B22/03 22:10
akr[m]which allows me to push omega into ℕ22/03 22:10
akr[m]but not sure what to do next22/03 22:10

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