haskell-ja > Archives > 2013/05/20

$ cat Test.agda
module Test where

data A : Set where
  a : A

data B : Set where
  b : B

idA : A → A
idA x = {!!}

idB : B → B
idB x = {!!}
$ agda -I Test.agda
Main> :typeOf x
1,1-2
Not in scope:
  x at 1,1-2
when scope checking x
Main> :typeIn 0 x
A
Main> :typeIn 1 x
B