Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/fold.agda
Created Mar 22, 2019

Embed
What would you like to do?
module Fold where
open import Level using (_⊔_)
open import Data.Nat asusing (ℕ; 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
You can’t perform that action at this time.