coq - 我可以使用 Inductive 类型的符号来在 Coq 中定义该类型吗？

Question

假设我有这样的东西:

Inductive SubtypeOf :
  Gamma -> UnsafeType -> Type -> Set :=
| SubRefl :
    forall (gamma : GammaEnv)  (u : UnsafeType)
    , SubtypeOf gamma u u
| SubTrans :
    forall (gamma : GammaEnv)  (u1 u2 u3 : Type)
    , SubtypeOf gamma u1 u2
      -> SubtypeOf gamma u2 u3
      -> SubtypeOf gamma u1 u3.

并定义了一个符号:

Notation "G |- x <: y " := (SubtypeOf G x y) (at level 50).

有什么方法可以将此符号纳入 SubtypeOf 的定义范围？ ，所以我可以这样做:

Inductive SubtypeOf :
  Gamma -> UnsafeType -> Type -> Set :=
| SubRefl :
    forall (gamma : GammaEnv)  (u : UnsafeType)
    ,  gamma |- u <: u
| SubTrans :
    forall (gamma : GammaEnv)  (u1 u2 u3 : Type)
    , gamma |- u1 <: u2
      -> gamma |- u2 <: u3
      -> gamma |- u1 <: u3.

Answer 1

扩展 ejgallego 的评论，有 Reserved Notation s 的文档和 a where clause for inductives .这是有效的代码:

Reserved Notation "G |-  x <: y" (at level 50, x at next level).
Definition UnsafeType := Type.
Axiom Gamma : Set.
Notation GammaEnv := Gamma.
Inductive SubtypeOf :
  Gamma -> UnsafeType -> Type -> Type :=
| SubRefl :
    forall (gamma : GammaEnv)  (u : UnsafeType)
    ,  gamma |- u <: u
| SubTrans :
    forall (gamma : GammaEnv)  (u1 u2 u3 : Type)
    , gamma |- u1 <: u2
      -> gamma |- u2 <: u3
      -> gamma |- u1 <: u3
where "G |-  x <: y " := (SubtypeOf G x y).

注意我们必须把x在下一级 (49)，因此 <:被解析为 |- , 而不是被吸收到 x .