agda_question.agda

module SQL where

open import Data.Nat

a : Nat
a = 1


{- 

nickolay@outpost:~/workspace/Agda/horn/src$ agda SQL.agda
Checking SQL (/home/nickolay/workspace/Agda/horn/src/SQL.agda).
     Loading  Agda.Builtin.Equality (/home/nickolay/.stack/snapshots/x86_64-linux/lts-11.9/8.2.2/share/x86_64-linux-ghc-8.2.2/Agda-2.5.3/lib/prim/Agda/Builtin/Equality.agdai).
     ...
     ...
     Loading  Agda.Builtin.Unit (/home/nickolay/.stack/snapshots/x86_64-linux/lts-11.9/8.2.2/share/x86_64-linux-ghc-8.2.2/Agda-2.5.3/lib/prim/Agda/Builtin/Unit.agdai).
     Loading  Data.Unit.Base (/home/nickolay/.agda/agda-stdlib-0.15/src/Data/Unit/Base.agdai).
  Loading  Data.Nat.Base (/home/nickolay/.agda/agda-stdlib-0.15/src/Data/Nat/Base.agdai).
 Loading  Data.Nat (/home/nickolay/.agda/agda-stdlib-0.15/src/Data/Nat.agdai).
/home/nickolay/workspace/Agda/horn/src/SQL.agda:5,5-8
Not in scope:
  Nat at /home/nickolay/workspace/Agda/horn/src/SQL.agda:5,5-8
when scope checking Nat

-}