Library Generic_Var
Module of variable definition
Module
Type
Generic_Var
.
Definition
Parameter
TVar
:
Type
.
We only require the decidability of equality over variables.
Parameter
eq_var_dec
:
forall
x
y
:
TVar
,
{
x
=
y
}
+
{
x
<>
y
}
.
End
Generic_Var
.