Skip to content

Instantly share code, notes, and snippets.

@ahmadsalim

ahmadsalim/Coll.agda Secret

Created February 6, 2017 15:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ahmadsalim/137f0455000e7c74547343e1af83bf2e to your computer and use it in GitHub Desktop.
Save ahmadsalim/137f0455000e7c74547343e1af83bf2e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Coll.agda
module Coll where
open import Size
data Coll (i : Size) (a : Set) : Set where
empty : Coll i a
single : a -> Coll i a
_∪_ : Coll i a -> Coll i a -> Coll i a
⋃ : ∀ {j : Size< i} → Coll i (Coll j a) -> Coll i a
-- How do I convince Agda this function terminates?
coll-map : ∀{a b i} -> (a -> b) -> Coll i a -> Coll i b
coll-map f empty = empty
coll-map f (single x) = single (f x)
coll-map f (c ∪ c₁) = coll-map f c ∪ coll-map f c₁
coll-map f (⋃ c) = ⋃ (coll-map (coll-map f) c)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment