这是我的 Coq 代码。
我期待着Check x ∪ y.表演x ∪ y，但是∪ {x, y}。
为什么？或者还有其他定义符号的想法吗？
我的 Coq 版本是 8.16.1。
Section Test.
Variable set:Type.
Variable In : set -> set -> Prop.
Notation "x ∈ y" := (In y x) (at level 50).
Structure class φ := {
class_base :> set;
class_row : forall x, x ∈ class_base <-> φ x;
}.
Axiom build_union : forall F, class (fun x => exists Y, x ∈ Y /\ Y ∈ F).
Notation "∪ F" := (build_union F) (at level 50).
Axiom build_non_ordered_pair_set : forall x y, class (fun w => w = x \/ w = y).
Notation "{ x , y }" := (build_non_ordered_pair_set x y) (at level 45).
Notation "x ∪ y" := (∪ {x, y}) (at level 50).
Variable F x y:set.
Check ∪ F.
(* ∪ F *)
(* : class (fun x : set => exists Y : set, x ∈ Y /\ Y ∈ F) *)
Check {x, y}.
(* {x, y} *)
(* : class (fun w : set => w = x \/ w = y) *)
Check x ∪ y.
(* ∪ {x, y} <- Why is not x ∪ y ? *)
(* : class (fun x0 : set => exists Y : set, x0 ∈ Y /\ Y ∈ {x, y}) *)
End Test.
我知道下面的代码运行良好。
Axiom build_two_union : forall x y, class (fun z => exists Y, z ∈ Y /\ Y ∈ {x, y}).
Notation "x ∪ y" := (build_two_union x y) (at level 2).
Check x ∪ y.