Skip to content

Instantly share code, notes, and snippets.

@canonic-epicure

canonic-epicure/agda_question.agda

Created May 16, 2018 15:11
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save canonic-epicure/f161745e899a0f072964bc89268e071b to your computer and use it in GitHub Desktop.
Save canonic-epicure/f161745e899a0f072964bc89268e071b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment