371392 (9) [Avatar] Offline
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
Yes, it should, thanks!