Skip to content

Instantly share code, notes, and snippets.

@mikesorae
Created July 10, 2019 06:20
Show Gist options
  • Save mikesorae/1f4374ca744332d87fab4b8ad7053877 to your computer and use it in GitHub Desktop.
Save mikesorae/1f4374ca744332d87fab4b8ad7053877 to your computer and use it in GitHub Desktop.
Idris lesson: proof of plus Zero + m = m
module Main
data N = Zero | Succ N
add : N -> N -> N
add Zero right = right
add (Succ left) right = Succ (add left right)
plusZeroRightNat : ( right : N ) -> add Zero right = right
plusZeroRightNat Zero = Refl
data Vector : N -> Type -> Type where
Empty : Vector Zero t
Cons : t -> Vector n t -> Vector (Succ n) t
concat : Vector n t -> Vector m t -> Vector (n `add` m) t
concat Empty ys = ys
concat (Cons x xs) ys = Cons x (concat xs ys)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment