Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active March 4, 2020 18:44
Show Gist options
  • Save gallais/e1e2053e234171799b9b034c19ed16cc to your computer and use it in GitHub Desktop.
Save gallais/e1e2053e234171799b9b034c19ed16cc to your computer and use it in GitHub Desktop.
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