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
.