[Agda] "Problem encountered. The *ghci* buffer perhaps can explain why"

Robert Rothenberg robrwo at gmail.com
Sat Jul 10 13:24:12 CEST 2010


I'm having trouble with Agda, installed from Ubuntu packages. "File
mode specification error. The *ghci* buffer perhaps can explain why".
In the buffer,

  <interactive>:1:0: Not in scope: `ioTCM'

  <interactive>:1:48: Not in scope: `cmd_write_highlighting_info'
  Prelude> ioTCM "/home/rr/src/Agda/Kripke.agda" Nothing ( cmd_goals
"/home/rr/src/Agda/Kripke.agda" )

  <interactive>:1:0: Not in scope: `ioTCM'

  <interactive>:1:48: Not in scope: `cmd_goals'
  Prelude>

Help!


More information about the Agda mailing list