Agda error: Not in scope when compiling example from documentation

Question

I have the following Agda file (named hellow-world.agda), taken straight from Agda documentation:

module hello-world where

  module B where
    f : Nat → Nat
    f n = suc n

  g : Nat → Nat → Nat
  g n m = m

But when I do Ctrl c, Ctrl l, I get the following error on emacs:

Not in scope:
  Nat at C:\Users\myname\Documents\Agda\hello-world.agda:4,9-12
when scope checking Nat

Answer 1

The example in the documentation is incomplete, it's there just to showcase the basics of the module system (although I do think it would be nice to make examples self-contained whenever possible).

Here's one way to make it type check, assuming you have agda-stdlib installed, which you probably do:

module hello-world where

  open import Data.Nat renaming (ℕ to Nat)

  module B where
    f : Nat → Nat
    f n = suc n

  g : Nat → Nat → Nat
  g n m = m

Or you can replace

  open import Data.Nat renaming (ℕ to Nat)

with

  data Nat : Set where
    zero : Nat
    suc : Nat -> Nat

Also note that the Agda documentation slightly misguides you here, normally the content of the top-level module isn't indented, i.e. most of the time people write

module hello-world where

open import Data.Nat renaming (ℕ to Nat)

module B where
  f : Nat → Nat
  f n = suc n

g : Nat → Nat → Nat
g n m = m

instead. Not that it's too important, just saves some horizontal space.