# Library Coq.micromega.VarMap

Require Import ZArith.
Require Import Coq.Arith.Max.
Require Import List.
Section MakeVarMap.
Variable A : Type.
Variable default : A.
Inductive t : Type :=
| Empty : t
| Leaf : A -> t
| Node : t -> A -> t -> t .
Fixpoint find (vm : t ) (p:positive) {struct vm} : A :=
match vm with
| Empty => default
| Leaf i => i
| Node l e r => match p with
| xH => e
| xO p => find l p
| xI p => find r p
end
end.
End MakeVarMap.