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