Lean 语言参考手册

关于：invalidDottedIdent🔗

Error code: lean.invalidDottedIdent

Dotted identifier notation used with invalid or non-inferrable expected type.

Severity: ErrorSince: 4.22.0

此错误表示在无效或不受支持的上下文中使用了点标识符记法。 点标识符记法允许省略标识符的命名空间，前提是 Lean 能根据类型信息推断它。关于该记法的详情请参阅 标识符章节。

该记法只能用于 Lean 能够推断其类型的项。如果类型信息不足，就会产生此错误。推断出的类型不能是类型 宇宙（例如 Prop 或 Type），因为这些类型不支持点标识符记法。

示例🔗

类型信息不足
def reverseDuplicate (xs : List α) := Invalid dotted identifier notation: The expected type of `.reverse` could not be determined Hint: Using one of these would be unambiguous: [apply] `Array.reverse` [apply] `BitVec.reverse` [apply] `List.reverse` [apply] `Vector.reverse` [apply] `List.IsInfix.reverse` [apply] `List.IsPrefix.reverse` [apply] `List.IsSuffix.reverse` [apply] `List.Sublist.reverse` [apply] `Lean.Grind.AC.Seq.reverse` [apply] `Std.DTreeMap.Internal.Impl.reverse` [apply] `Std.Tactic.BVDecide.BVUnOp.reverse` [apply] `Std.DTreeMap.Internal.Impl.Ordered.reverse`.reverse (xs ++ xs) 
Invalid dotted identifier notation: The expected type of `.reverse` could not be determined

Hint: Using one of these would be unambiguous:
  [apply] `Array.reverse`
  [apply] `BitVec.reverse`
  [apply] `List.reverse`
  [apply] `Vector.reverse`
  [apply] `List.IsInfix.reverse`
  [apply] `List.IsPrefix.reverse`
  [apply] `List.IsSuffix.reverse`
  [apply] `List.Sublist.reverse`
  [apply] `Lean.Grind.AC.Seq.reverse`
  [apply] `Std.DTreeMap.Internal.Impl.reverse`
  [apply] `Std.Tactic.BVDecide.BVUnOp.reverse`
  [apply] `Std.DTreeMap.Internal.Impl.Ordered.reverse`
def reverseDuplicate (xs : List α) : List α := .reverse (xs ++ xs)

由于未指定 reverseDuplicate 的返回类型，无法确定 .reverse 的期望类型。Lean 不会使用参数 xs ++ xs 的类型推断省略的命名空间。添加返回类型 List α 后，Lean 就能推断 .reverse 的类型，进而推断解析该标识符所需的命名空间（List）。

注意，这意味着改变 reverseDuplicate 的返回类型会改变 .reverse 的解析方式：如果返回类型是 T， Lean 会尝试将 .reverse 解析为函数 T.reverse，其返回类型是 T——即使 T.reverse 不接受类型为 List α 的参数。

应为类型宇宙处使用点标识符
example (n : Nat) := match n > 42 with | Invalid dotted identifier notation: Not supported on type universe Prop.true => n - 1 | .false => n + 1 
Invalid dotted identifier notation: Not supported on type universe
  Prop
example (n : Nat) := match decide (n > 42) with | .true => n - 1 | .false => n + 1

命题 n > 42 的类型是 Prop；由于它是类型宇宙，不支持点标识符记法。如本例所示，在这种 上下文中使用该记法几乎总是错误。此例原本想让 .true 和 .false 表示布尔值，而非命题；不过， Lean.Parser.Term.match : termmatch 表达式不会自动对可判定命题执行这种强制转换。显式添加 decide 会使判别式成为 Bool，从而使点标识符解析成功。