存在于 where 外部范围内的值的“未定义名称”答案

【问题标题】："Undefined name" for value present in outer scope of where存在于 where 外部范围内的值的“未定义名称”
【发布时间】：2021-03-14 15:11:06
【问题描述】：

我想使用在 where 子句的外部范围中定义的值，就像这样

foo : Nat
foo = case Just 1 of
  Nothing => 0
  Just x => bar where
    bar : Nat
    bar = x

但我得到了

Error: While processing right hand side of foo. While processing right hand side of foo,bar. Undefined name x. 

Foo.idr:30:11--30:12
    |
 30 |     bar = x

鉴于the docs 中所说的内容，我不明白这一点

在外部范围内可见的任何名称在 where 子句中也可见（除非它们已被重新定义，例如此处的 xs）。出现在类型中的名称将在 where 子句的范围内。

将 x 绑定到 RHS 上的新名称

foo : Nat
foo = case Just 1 of
  Nothing => 0
  Just x => let x' = x in bar where
    bar : Nat
    bar = x'

导致Undefined name x' 出现类似的错误bar = x'

【问题讨论】：

标签： scope idris

【解决方案1】：

您似乎在寻找 let 而不是 where。外部范围意味着foo 的参数。

【讨论】：

hmmm ...在我的实际代码中，bar 是一元函数，我将其返回。我可以用let 做到这一点，但是在我定义内部函数的地方使用where 感觉更自然。如果有帮助，我可以扩展我的示例
外部范围是否包含with 组件？
@joel 也许吧。试试看。它应该会看到 LHS 中定义的任何内容。