Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active Mar 4, 2020
Embed
What would you like to do?
Terminating map via commuting conversions
Inductive Tree (A : Set) : Set :=
| Leaf : A -> Tree A
| Node : bool -> Tree A * Tree A -> Tree A.
Definition subTree {A : Set} (b : bool) (lr : Tree A * Tree A) : Tree A :=
match (b, lr) with
| (true, (a, b)) => a
| (false, (a, b)) => b
end.
Fixpoint get {A : Set} (t : Tree A) : A :=
match t with
| Leaf _ a => a
| Node _ b lr => get (subTree b lr)
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment