search

Smaug123 / agdaproofs

Mathematical proofs in Agda
MIT License
4 stars 1 forks source link

Subtraction #45

Closed Smaug123 closed 5 years ago

Smaug123 commented 5 years ago

As of the raising of this PR, we're not really done. We have defined subtraction, and shown that it respects canonical, but not that it is the same as unary subtraction.

Smaug123 commented 5 years ago

As of this point, we have defined subtraction and shown that a <N b if and only if (NToBinNat a) -B (NToBinNat b) is no.

We still need to show that a <N b allows us to perform a unary subtraction which corresponds to -B.

Smaug123 commented 5 years ago

Fixes #29 .