Skip to content

Instantly share code, notes, and snippets.

@anton-trunov
Last active May 10, 2017 06:35
Show Gist options
  • Save anton-trunov/0c2d21b770d350646e5f0a4e8a8072f4 to your computer and use it in GitHub Desktop.
Save anton-trunov/0c2d21b770d350646e5f0a4e8a8072f4 to your computer and use it in GitHub Desktop.
--http://stackoverflow.com/questions/43879173/in-idris-use-rewrite-under-a-lambda
%default total
sum : List Nat -> Nat
sum [] = 0
sum (x :: xs) = x + sum xs
sum_cont' : {a : Type} -> List Nat -> (Nat -> a) -> a
sum_cont' [] k = k 0
sum_cont' (x :: xs) k = sum_cont' xs (k . (+ x))
sum_cont : List Nat -> Nat
sum_cont l = sum_cont' l id
sum_cont_correct' : (k : Nat -> ty) -> (xs : List Nat) -> sum_cont' xs k = k (sum xs)
sum_cont_correct' k [] = Refl
sum_cont_correct' k (x :: xs) =
rewrite plusCommutative x (sum xs) in
sum_cont_correct' (k . (+ x)) xs
sum_cont_correct : (xs : List Nat) -> sum_cont xs = sum xs
sum_cont_correct = sum_cont_correct' id
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment