Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/vwrong.idr

Created July 17, 2014 15:49
Show Gist options
  • Save edwinb/4646af7cbf0aac144dea to your computer and use it in GitHub Desktop.
Save edwinb/4646af7cbf0aac144dea to your computer and use it in GitHub Desktop.
Download ZIP
Raw
vwrong.idr
vapp : Vect n a -> Vect m a -> Vect (m + n) a
vapp [] ys ?= {vapp_nil_lemma} ys
vapp (x :: xs) ys ?= {vapp_cons_lemma} x :: vapp xs ys
---------- Proofs ----------
Main.vapp_cons_lemma = proof
intros
rewrite (plusSuccRightSucc m n)
trivial
Main.vapp_nil_lemma = proof
intros
rewrite sym (plusZeroRightNeutral m)
trivial
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment