[Agda] Instead of a REPL

Eduardo Ochs eduardoochs at gmail.com
Fri Feb 4 17:38:32 CET 2022

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...


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


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!

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

More information about the Agda mailing list