<div dir="ltr">Hi all,<br><br>this is an answer to the discussion on REPLs on the thread below,<br>but I thought that this deserves a new thread and a new title...<br><br>  <a href="https://lists.chalmers.se/pipermail/agda/2022/thread.html#12862">https://lists.chalmers.se/pipermail/agda/2022/thread.html#12862</a><br>  <a href="https://lists.chalmers.se/pipermail/agda/2022/012862.html">https://lists.chalmers.se/pipermail/agda/2022/012862.html</a><br>  <a href="https://lists.chalmers.se/pipermail/agda/2022/012867.html">https://lists.chalmers.se/pipermail/agda/2022/012867.html</a><br><br>Here is a simple hack that does most of what I need from a REPL:<br><br>  <a href="http://angg.twu.net/AGDA/find-agdatype.el.html">http://angg.twu.net/AGDA/find-agdatype.el.html</a><br>  <a href="http://angg.twu.net/AGDA/find-agdatype.el">http://angg.twu.net/AGDA/find-agdatype.el</a><br><br>Here's how to test it. Run this,<br><br>  rm -Rv /tmp/agdanonrepl/<br>  mkdir  /tmp/agdanonrepl/<br>  cd     /tmp/agdanonrepl/<br>  wget <a href="http://angg.twu.net/AGDA/find-agdatype.el">http://angg.twu.net/AGDA/find-agdatype.el</a><br>  wget <a href="http://angg.twu.net/AGDA/Postulate1.agda">http://angg.twu.net/AGDA/Postulate1.agda</a><br><br>and then this,<br><br>  (load      "/tmp/agdanonrepl/find-agdatype.el")<br>  (find-file "/tmp/agdanonrepl/Postulate1.agda")<br><br>then make Agda load Postulate1.agda with `C-c C-l', and execute the<br>sexps like<br><br>  -- (find-agdatype  ...)<br>  -- (find-agdatypep ...)<br>  -- (find-agdanorm  ...)<br>  -- (find-agdanormp ...)<br><br>in Postulate1.agda "by hand" and watch what they show in the second<br>window. The file Postulate1.agda has lots of sexps that depend on eev,<br>but you can ignore them.<br><br>Note that the current version of find-agdatype.el:<br><br>  1) does not depend on eev (the previous one did),<br>  2) is less than one hour old now,<br>  3) needs better tests and examples.<br><br>I hope that this is useful!<br>All feedback very welcome!<br>  Cheers,<br><br>    Eduardo Ochs<br>    <a href="http://angg.twu.net/eev-agda.html">http://angg.twu.net/eev-agda.html</a><br>    <a href="http://angg.twu.net/#eev">http://angg.twu.net/#eev</a><br><div><br></div></div>