Anonymous user
Talk:Proof: Difference between revisions
m
→Quantifiers: add zero-width spaces to enable better line breaking
(→J version: Add some notes on the Tcl code (and the fact that implementing a whole theorem prover for this task is unreasonable!); also tidy formatting) |
m (→Quantifiers: add zero-width spaces to enable better line breaking) |
||
Line 241:
::: > My current inclination is to believe that you treat some "failures" as "valid for purposes of proof" in your implementation of types
::: By "you" you mean anybody who "believe" in Agda/
:::: If your description here is correct, then these implementations of homotopy type theory have weaknesses in their treatment of upper bounds. No big deal, perhaps, except that you seem rather intolerant of other implementations with the same kind of limitation. --[[User:Rdm|Rdm]] 01:53, 14 May 2012 (UTC)
| |||