[Agda] Instead of a REPL

[Eduardo Ochs]

Hi all,

this is an answer to the discussion on REPLs on the thread below,
but I thought that this deserves a new thread and a new title...

  https://lists.chalmers.se/pipermail/agda/2022/thread.html#12862
  https://lists.chalmers.se/pipermail/agda/2022/012862.html
  https://lists.chalmers.se/pipermail/agda/2022/012867.html

Here is a simple hack that does most of what I need from a REPL:

  http://angg.twu.net/AGDA/find-agdatype.el.html
  http://angg.twu.net/AGDA/find-agdatype.el

Here's how to test it. Run this,

  rm -Rv /tmp/agdanonrepl/
  mkdir  /tmp/agdanonrepl/
  cd     /tmp/agdanonrepl/
  wget http://angg.twu.net/AGDA/find-agdatype.el
  wget http://angg.twu.net/AGDA/Postulate1.agda

and then this,

  (load      "/tmp/agdanonrepl/find-agdatype.el")
  (find-file "/tmp/agdanonrepl/Postulate1.agda")

then make Agda load Postulate1.agda with `C-c C-l', and execute the
sexps like

  -- (find-agdatype  ...)
  -- (find-agdatypep ...)
  -- (find-agdanorm  ...)
  -- (find-agdanormp ...)

in Postulate1.agda "by hand" and watch what they show in the second
window. The file Postulate1.agda has lots of sexps that depend on eev,
but you can ignore them.

Note that the current version of find-agdatype.el:

  1) does not depend on eev (the previous one did),
  2) is less than one hour old now,
  3) needs better tests and examples.

I hope that this is useful!
All feedback very welcome!
  Cheers,

    Eduardo Ochs
    http://angg.twu.net/eev-agda.html
    http://angg.twu.net/#eev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220204/a0f3b59f/attachment.html>