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

Question

我想使用在 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

鉴于文档中的内容，我不明白这一点

在外部范围内可见的任何名称在 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'

标签： scopeidris

Answer 1

你似乎在寻找let不where。外部范围意味着foo.