coe
[coe]
属性は、特定の関数を型強制を行う関数として登録し、↑
記号で表示されるようにします。
/-- 自前で定義した自然数 -/
inductive MyNat where
| zero : MyNat
| succ : MyNat → MyNat
-- `MyNat.succ` を(意味をなしていないが)型強制として登録する
attribute [coe] MyNat.succ
-- `MyNat.succ` ではなく `↑` と表示されるようになった
/-- info: ↑MyNat.zero : MyNat -/
#guard_msgs in
#check (MyNat.succ .zero : MyNat)
用途
型強制を Coe
型クラスで登録しただけでは、必ずしも型強制を行う関数が ↑
記号で表示されるわけではありません。[coe]
属性を付与することにより、より「型強制らしく」表示されるようになります。
/-- 自然数の組 -/
def IntBase := Nat × Nat
/-- 自然数の組に対する同値関係 -/
def IntBase.equiv : IntBase → IntBase → Prop :=
fun (a₁, b₁) (a₂, b₂) => a₁ + b₂ = b₁ + a₂
/-- `IntBase` 上の同値関係として `IntBase.equiv` を登録する -/
instance IntBase.setoid : Setoid IntBase where
r := IntBase.equiv
iseqv := by
constructor
case refl =>
intro ⟨x, y⟩
dsimp [IntBase.equiv]
ac_rfl
case symm =>
intro ⟨x, y⟩ ⟨x', y'⟩ h
dsimp [IntBase.equiv] at *
omega
case trans =>
intro ⟨x, y⟩ ⟨x', y'⟩ ⟨x'', y''⟩ hxy hyz
dsimp [IntBase.equiv] at *
omega
/-- 整数を表す型 -/
abbrev myInt := Quotient IntBase.setoid
/-- 自然数を `myInt` に変換する -/
def myInt.ofNat (n : Nat) : myInt := Quotient.mk' (n, 0)
/-- `Nat → myInt` という型強制 -/
instance : Coe Nat myInt where
coe := myInt.ofNat
-- この時点では、`myInt.ofNat` が型強制として表示されない
/-- info: myInt.ofNat Nat.zero : myInt -/
#guard_msgs in
#check (Nat.zero : myInt)
-- `[coe]` 属性を付与する
attribute [coe] myInt.ofNat
-- `myInt.ofNat` ではなく `↑` と表示されるようになった!
/-- info: ↑Nat.zero : myInt -/
#guard_msgs in
#check (Nat.zero : myInt)