3.7. 额外的便利语法
3.7.1. 实例的构造子语法
在幕后，类型类是结构类型，而实例是这些类型的值。
二者唯一的区别是，Lean 会存储关于类型类的额外信息，例如哪些参数是输出参数，并且实例会被注册以供搜索。
虽然具有结构类型的值通常使用 ⟨...⟩ 语法，或使用花括号和字段来定义，而实例通常使用 where 来定义，但这两种语法都适用于这两类定义。
例如，一个林业应用程序可以如下表示树木：
structure Tree : Type where
latinName : String
commonNames : List String
def oak : Tree :=
⟨"Quercus robur", ["common oak", "European oak"]⟩
def birch : Tree :=
{ latinName := "Betula pendula",
commonNames := ["silver birch", "warty birch"]
}
def sloe : Tree where
latinName := "Prunus spinosa"
commonNames := ["sloe", "blackthorn"]这三种语法都是等价的。
类似地，类型类实例可以用全部三种语法来定义：
class Display (α : Type) where
displayName : α → String
instance : Display Tree :=
⟨Tree.latinName⟩
instance : Display Tree :=
{ displayName := Tree.latinName }
instance : Display Tree where
displayName t := t.latinName
where 语法通常用于实例，而结构则使用花括号语法或 where 语法。
当需要强调某个结构类型非常类似于一个元组，只是其字段恰好带有名称、而这些名称在当前并不重要时，⟨...⟩ 语法会很有用。
然而，在某些情况下，使用其他替代方式也是合理的。
特别地，库可能会提供一个构造实例值的函数。
在实例声明中的 := 之后放置对该函数的调用，是使用这种函数的最简单方式。
3.7.2. 示例
在试验 Lean 代码时，定义可能比 #eval 或 #check 命令更便于使用。
首先，定义不会产生任何输出，这有助于使读者的注意力集中在最有意思的输出上。
其次，编写大多数 Lean 程序时，最容易的做法是从类型签名开始，让 Lean 在编写程序本身时提供更多帮助和更好的错误消息。
另一方面，#eval 和 #check 在 Lean 能够根据所给表达式确定类型的上下文中最容易使用。
第三，#eval 不能用于其类型没有 ToString 或 Repr 实例的表达式，例如函数。
最后，多步骤的 do 块、let 表达式以及其他占多行的语法形式，若要在 #eval 或 #check 中带类型标注来书写，会尤其困难，原因只是所需的括号化可能难以预料。