--- Day changed Wed Mar 22 2017 | ||

MathUser | Can 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 |
---|---|---|

apostolis | If 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/ec9b4740e025a70c9e87c35be99b592a | 22/03 21:51 |

akr[m] | any ideas? | 22/03 21:51 |

akr[m] | it seems like I should use the existence of omega somehow | 22/03 22:10 |

akr[m] | I've got a lemma that A ≡ B → A → B | 22/03 22:10 |

akr[m] | which allows me to push omega into ℕ | 22/03 22:10 |

akr[m] | but not sure what to do next | 22/03 22:10 |

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