Skip to content

Instantly share code, notes, and snippets.

@oisdk
Created March 22, 2019 01:26
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save oisdk/8a656a683ec769afb3628839b3f2c159 to your computer and use it in GitHub Desktop.
module Fold where
open import Level using (_⊔_)
open import Data.Nat as ℕ using (ℕ; suc; zero; _+_)
open import Data.List hiding (sum)
open import Relation.Binary.PropositionalEquality
record Fold {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
field
⟦_⟧[] : B
⟦_⟧_∷_ : A B B
⟦_⟧ = foldr ⟦_⟧_∷_ ⟦_⟧[]
open Fold
sum : Fold ℕ ℕ
⟦ sum ⟧[] = 0
⟦ sum ⟧ x ∷ xs = x + xs
_ : ⟦ sum ⟧ (21 ∷ []) ≡ 3
_ = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment