Skip to content

Instantly share code, notes, and snippets.

@kmill

kmill/mirror_tree.lean

Last active June 19, 2020 21:08
Show Gist options
  • Save kmill/8650f23482a60baa39299ab9ec9ee765 to your computer and use it in GitHub Desktop.
Save kmill/8650f23482a60baa39299ab9ec9ee765 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
mirror_tree.lean
inductive binary_tree : Type
| root : binary_tree
| tree : binary_tree → binary_tree → binary_tree
namespace binary_tree
def mirror : binary_tree → binary_tree
| root := root
| (tree a b) := tree (mirror b) (mirror a)
end binary_tree
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment