Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
plus commutes
plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
-- Base case
(O + m = m + O) <== plus_comm =
rewrite ((m + O = m) <== plusZeroRightNeutral) ==>
(O + m = m) in refl
-- Step case
(S k + m = m + S k) <== plus_comm =
rewrite ((k + m = m + k) <== plus_comm) in
rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
refl
-- QED
@LeifW

This comment has been minimized.

Copy link

commented Jan 24, 2016

This is linked as a syntax example from release notes (http://www.idris-lang.org/idris-0-9-9-released/), but has bitrotted. A up-to-date example version of this can be found in the tests: https://github.com/idris-lang/Idris-dev/blob/master/test/proof001/test029.idr

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.