agdaagda-mode

Agda error: Not in scope when compiling example from documentation


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

Solution

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