Talk:Proof: Difference between revisions
→Quantifiers
m (Simplify) |
|||
Line 252:
::::: "Upper bounds" makes sense for brute-forcing "proofs" but the real proof systems uses unification... Well, it's still required to get the point. Talking about the "upper bounds" is not even funny :) — [[User:Ht|Ht]] 07:33, 14 May 2012 (UTC)
:::::: And that's fine, until you start asking people to implement these infinite concepts as types. To use your turn of phrase, that's "not even funny :)". --[[User:Rdm|Rdm]] 11:53, 14 May 2012 (UTC)
::: My current inclination is to believe that you cannot get [http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf the point] of dependently-typed programming languages / proof systems. — [[User:Ht|Ht]] 23:00, 13 May 2012 (UTC)
| |||