13.10. Type 归属🔗

Type ascriptions 用术语的类型显式注释它们。它们是为 Lean 提供术语的预期类型的一种方法。此类型在定义上必须等于基于术语上下文所期望的类型。 Type 归属不仅仅用于记录程序：

程序文本中可能没有足够的信息来派生术语的类型。归属是提供类型的一种方式。
推断的类型可能不是某个术语所需的类型。
术语的预期类型用于驱动强制转换的插入，而归属是控制强制插入位置的一种方法。

syntaxPostfix Type Ascriptions

Type 归属必须用括号括起来。它们表明第一项的类型是第二项。

term ::= ...
    | Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
([anonymous]term : term)

如果需要类型归属的术语很长，例如策略证明或 Lean.Parser.Term.do : termdo 块，则带有强制括号的后缀类型归属可能难以阅读。此外，对于证明和 Lean.Parser.Term.do : termdo 块，术语的类型对其解释至关重要。在这些情况下，前缀版本可以更容易阅读。

syntaxPrefix Type Ascriptions

term ::= ...
    | show term from term

当Lean.Parser.Term.show : termshow主体中的术语是策略证明时，可以省略关键字Lean.Parser.Term.show : termfrom。

term ::= ...
    | show term by A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. tacticSeq

Ascribing Statements to Proofs

此示例无法执行策略证明，因为所需的命题未知。作为运行早期策略的一部分，该命题会自动细化为策略可以证明的命题。然而，他们的默认情况填写不正确，导致证明失败。

example (n : Nat) := byn:Nat⊢ ?m.2 n
  induction nzero⊢ ?m.2 0succn✝:Nata✝:?m.2 n✝⊢ ?m.2 (n✝ + 1)
  next =>⊢ ?m.2 0 rflAll goals completed! 🐙
  next n' ih =>n':Natih:0 ≍ n'⊢ 0 ≍ n' + 1
    simp only [HAdd.hAdd, Add.add, Nat.add] at *n':Natih:0 ≍ n'⊢ 0 ≍ n'.succ
    rewrite [Invalid rewrite argument: Expected an equality or iff proof or definition name, but `ih` is a proof of
  0 ≍ n'ihn':Natih:0 ≍ n'⊢ 0 ≍ n'.succ]n':Natih:0 ≍ n'⊢ 0 ≍ n'.succ
    rfl

Invalid rewrite argument: Expected an equality or iff proof or definition name, but `ih` is a proof of
  0 ≍ n'

具有 Lean.Parser.Term.show : termshow 的前缀类型归属可用于提供正在证明的命题。这在语法上下文中很有用，因为将其添加为本地定义会很不方便。

example (n : Nat) := show 0 + n = n byAll goals completed! 🐙
  induction nzero⊢ 0 + 0 = 0succn✝:Nata✝:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
  next =>⊢ 0 + 0 = 0 rflAll goals completed! 🐙
  next n' ih =>n':Natih:0 + n✝ = n✝⊢ 0 + (n✝ + 1) = n✝ + 1
    simp only [HAdd.hAdd, Add.add, Nat.add] at *n':Natih:Nat.add 0 n' = n'⊢ (Nat.add 0 n').succ = n'.succ
    rewrite [ihn':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ]n':Natih:Nat.add 0 n' = n'⊢ n'.succ = n'.succ
    rflAll goals completed! 🐙

Live ↪

Ascribing Types to Lean.Parser.Term.do : termdo Blocks

此示例缺乏足够的类型信息来合成 Pure 实例。

example := do
  typeclass instance problem is stuck
  Pure ?m.12

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.return 5

typeclass instance problem is stuck
  Pure ?m.12

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Pure` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

具有 Lean.Parser.Term.show : termshow 的前缀类型归属与 hole 一起可用于指示 monad。默认 OfNat _ 5 实例提供了足够的类型信息来填充 Nat 的漏洞。

example := show StateM String _ from do
  return 5

Live ↪

后缀类型归属和 Lean.Parser.Term.show : termshow 之间存在重要区别。普通后缀类型归属会更改该术语的预期类型，这可能会改变该术语的详细说明方式。然而，在精化之后，Lean 推断结果项的类型，并使用该推断类型执行进一步的精化任务。另一方面，Lean.Parser.Term.show : termshow 详细精化了推断类型为归属类型的术语。使用通用字段表示法时可以观察到差异，其中仅保证在使用 Lean.Parser.Term.show : termshow 时使用归属类型来解析字段。

Postfix Ascription vs show

此定义为 List String 建立了替代名称：

def Colors := List String

后缀类型归属提供了确定隐式参数 String 到 List.nil 所需的类型信息，但结果类型仍然是 List String：

[] : List String#check ([] : Colors)

[] : List String

另一方面，当使用 Lean.Parser.Term.show : termshow 时，详细术语的构造方式使得推断类型为 Colors：

have this := [];
this : Colors#check (show Colors from [])

have this := [];
this : Colors

该函数设计为使用通用字段表示法调用：

def Colors.hasYellow (cs : Colors) : Bool :=
  cs.any (·.toLower == "yellow")

由于它们推断类型的差异，它可以与 Lean.Parser.Term.show : termshow 一起使用，但不能与后缀类型归属一起使用：

#eval ([] : Colors).Invalid field `hasYellow`: The environment does not contain `List.hasYellow`, so it is not possible to project the field `hasYellow` from an expression
  []
of type `List String`hasYellow

Invalid field `hasYellow`: The environment does not contain `List.hasYellow`, so it is not possible to project the field `hasYellow` from an expression
  []
of type `List String`

false#eval (show Colors from []).hasYellow

false