This file contains 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
-- This is the type we're working with. | |
data List a = List (forall r. (a -> r -> r) -> r -> r) | |
-- Implement this signature. It should not be inefficient, so if you're planning | |
-- on writing something like tail (notoriously inefficient using foldr) on our | |
-- List type, think again! It should be possible to write with the same time | |
-- complexity as the original. And of course, converting to/from a conventional | |
-- list is cheating :) | |
zipWith :: (a -> b -> c) -> List a -> List b -> List c |
This file contains 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
module Nicomachus where | |
open import Function | |
open import Relation.Binary.PropositionalEquality | |
import Relation.Binary.EqReasoning as EqReasoning | |
open import Data.Nat | |
open import Data.Nat.Properties | |
-- http://en.wikipedia.org/wiki/Nicomachus%27s_theorem |