`abbrev`¶

abbrev は略記を作るコマンドです． def と似ていますが，「新しい概念を作る」というより「長い型や式に短い名前をつける」という意図を表します． Lean は abbrev を展開しやすい略記として扱うので，型の同一視や型推論で邪魔になりにくいです．一方で，数学的に意味のある新しい概念や，後で定理を付けたい対象には def を使うことが多いです．

abbrev NatPair := Nat × Nat

def sumNatPair (p : NatPair) : Nat :=
  p.1 + p.2

example : sumNatPair (2, 3) = 5 := by
  rfl

NatPair は Nat × Nat の略記なので，Lean は両者をほとんど同じものとして扱います．このため，Nat × Nat 型の値をそのまま NatPair として使えます．

example (p : Nat × Nat) : NatPair := p

abbrev¶

`abbrev`¶