atttibute [coe]でインフォビュー上での表示を↑に換える

[Seasawher]

MILで，CoeFun の表示を変えるという話があった

[Seasawher]

Nat.succ を Coe ぽく表示できる

attribute [coe] Nat.succ
#check Nat.succ 1

[Seasawher]

普通は Coe のインスタンスにするだけで十分だが、それで上手くいかないときもあって、手動で付与する羽目になることがある

[Seasawher]

coe 属性が必要な例

def IntBase := Nat × Nat

def IntBase.equiv : IntBase → IntBase → Prop :=
  fun (a₁, b₁) (a₂, b₂) => a₁ + b₂ = b₁ + a₂

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

def myInt.ofNat (n : Nat) : myInt := ⟦(n, 0)⟧

instance : Coe Nat myInt where
  coe := myInt.ofNat

/-- info: myInt.ofNat Nat.zero : myInt -/
#guard_msgs in
  #check (Nat.zero : myInt)

attribute [coe] myInt.ofNat

/-- info: ↑Nat.zero : myInt -/
#guard_msgs in
  #check (Nat.zero : myInt)