Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment