Revision as of 07:18, 1 June 2012 (view source) rosettacode>Ht (update the task and agda example) ← Older edit		Revision as of 07:20, 1 June 2012 (view source) rosettacode>Ht mNo edit summary Newer edit →
Line 194: -- ?1 : 2×ℕ+1 (.m + .n) -- -- but 2×ℕ+1 (zero + zero) = 2×ℕ+1 0 which is ~~uninhabiten~~uninhabited, so that this proof -- can not be writen. --

Proof: Difference between revisions

Proof (view source)