Skip to content

Instantly share code, notes, and snippets.

@mvr

mvr/Test.idr

Last active March 4, 2016 20:22
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 mvr/db2288afad6f9e2ba5ca to your computer and use it in GitHub Desktop.
Save mvr/db2288afad6f9e2ba5ca to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Test.idr
module Test
data Chain : Nat -> Type where
MkChain : List (String, Nat) -> Chain n
data Map : Nat -> Type where
MkMap : (Chain n -> Chain (n + d)) -> Map d
compose : Map df -> Map dg -> Map (dg + df)
compose (MkMap f) (MkMap g) = MkMap go
where go ch = f (g ch)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment