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
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.