371392 (9) [Avatar] Offline
#1
V13, section 8.6.2:

“By using Dec, you’ve been able to write explicitly in the type what checkEqNat is supposed to do: run either a proof that the inputs are equal, or a proof that they’re not.”


Should this be “return either a proof […]”?
Edwin Brady (65) [Avatar] Offline
#2
Yes, it should, thanks!