mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
7 lines
179 B
Coq
7 lines
179 B
Coq
Require Import String.
|
|
|
|
|
|
Definition var := string.
|
|
Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec.
|
|
|
|
Infix "==v" := var_eq (no associativity, at level 50).
|