Search code examples
scopeidris

"Undefined name" for value present in outer scope of where

I want to use a value defined in the outer scope of a where clause, like so

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

but I'm getting

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

I don't understand this given what it says in the docs

Any names which are visible in the outer scope are also visible in the where clause (unless they have been redefined, such as xs here). A name which appears in the type will be in scope in the where clause.

Binding x to a new name on the RHS

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

results in a similar error Undefined name x' for bar = x'

Solution

  • You appear to be looking for let not where. Outer scope means arguments to foo.