Skip to content

Instantly share code, notes, and snippets.

@thomasdziedzic

thomasdziedzic/flip_tree.idr

Last active October 26, 2015 06: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 thomasdziedzic/c6fe1df8847656ebf2f9 to your computer and use it in GitHub Desktop.
Save thomasdziedzic/c6fe1df8847656ebf2f9 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
flip_tree.idr
module Tree
%default total
data Tree : Type -> Type where
Leaf : Tree a
Branch : (ltree : Tree a) -> a -> (rtree : Tree a) -> Tree a
flip : Tree a -> Tree a
flip Leaf = Leaf
flip (Branch ltree x rtree) = Branch (flip rtree) x (flip ltree)
flipFlip : (t : Tree a) -> flip (flip t) = t
flipFlip Leaf = Refl
flipFlip (Branch ltree x rtree) =
rewrite flipFlip ltree in
rewrite flipFlip rtree in
Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment