abbrev

abbrev は、略称(abbreviation)を宣言するコマンドです。

たとえば、Nat 型に別の名前を与えたかったとしましょう。Lean では型も他の項と同様に宣言できるので、次のように書いて問題がないように見えます。

def NaturalNumber : Type := Nat

しかし、ここで定義した Nat の別名を項に対して使用するとエラーになります。エラーメッセージには以下の通り「NaturalNumber の OfNat インスタンスが見つかりません」という旨のことが書かれています。これは、Lean が NaturalNumber を定義に簡約(reduce)するよりも先に、42 : NaturalNumber という表記が定義されているか OfNat のインスタンスを探そうとしてエラーになったことを示唆します。

/--
error: failed to synthesize
  OfNat NaturalNumber 42
numerals are polymorphic in Lean, but the numeral `42` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in #check (42 : NaturalNumber)

ここでエラーを修正する方法の一つが、def の代わりに abbrev を使用することです。

abbrev NaturalNumber : Type := Nat

#check (42 : NaturalNumber)

舞台裏

abbrev は [reducible] 属性のついた def と同じであり、定義に [reducible] 属性を与えても同様のことができます。

@[reducible] def NaturalNumber : Type := Nat

#check (42 : NaturalNumber)