Created
August 3, 2019 04:41
-
-
Save MarcelineVQ/4e1ae23c9a8dcb9c398f1c6e3a9f3ee7 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| adjacent: (x, y : BitVector n) -> Dec (hammingDistance x y = 1) | |
| adjacent x y with (hammingDistance x y) | |
| adjacent x y | Z = No (\Refl impossible) | |
| adjacent x y | (S Z) = Yes Refl | |
| adjacent x y | (S (S k)) = No (\Refl impossible) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment