Skip to content

Instantly share code, notes, and snippets.

Created Jul 10, 2019
What would you like to do?
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