Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/Snoc.idr

Created April 2, 2015 13:58
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 david-christiansen/195080f0cecb295699ca to your computer and use it in GitHub Desktop.
Save david-christiansen/195080f0cecb295699ca to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Snoc.idr
module Snoc
data SnocList : List a -> Type where
SnocNil : SnocList []
Snoc : (xs : List a) -> (x : a) -> SnocList (xs ++ [x])
snocList : (xs : List a) -> SnocList xs
snocList [] = SnocNil
snocList (x :: xs) with (snocList xs)
snocList (x :: []) | SnocNil = Snoc [] x
snocList (x :: (ys ++ [y])) | (Snoc ys y) = Snoc (x::ys) y
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment