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

问题描述

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

解决方法

您似乎在寻找 let 而不是 where。外部作用域表示 foo 的参数。