<div dir="ltr">Hi Thorsten,<div><br></div><div>These are the 3 files that they could be in, but it's been a while so I don't remember where I did the configuration:</div><div><a href="https://github.com/larrytheliquid/thesis/blob/master/paper/agda.sty">https://github.com/larrytheliquid/thesis/blob/master/paper/agda.sty</a><br></div><div><a href="https://github.com/larrytheliquid/thesis/blob/master/paper/psu-thesis.sty">https://github.com/larrytheliquid/thesis/blob/master/paper/psu-thesis.sty</a><br></div><div><a href="https://github.com/larrytheliquid/thesis/blob/master/paper/thesis.tex">https://github.com/larrytheliquid/thesis/blob/master/paper/thesis.tex</a><br></div><div><br></div><div>However, it looks like the newest agda.sty has more configuration options than it did years ago:</div><div><a href="https://github.com/agda/agda/blob/master/src/data/agda.sty">https://github.com/agda/agda/blob/master/src/data/agda.sty</a><br></div><div><br></div><div>For example, it might be enough to turn off the initial space around code:</div><div><span style="color:rgb(0,92,197);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">\AgdaNoSpaceAroundCode</span><br></div><div>There's more config options and commands related to this but I'm unfamiliar with them.</div><div><br></div><div>Also, it looks like AgdaHide still exists (<a href="https://github.com/agda/agda/blob/master/src/data/agda.sty#L339-L343">https://github.com/agda/agda/blob/master/src/data/agda.sty#L339-L343</a>)<br></div><div>but is deprecated in favor of <span style="color:rgb(106,115,125);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">begin{code}[hide]</span></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Aug 2, 2020 at 11:39 AM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-GB">
<div class="gmail-m_-5776715658570266716WordSection1">
<p class="MsoNormal"><span>Hi Larry,<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Thank you for your email. Yes, this sounds like a good idea. Ok I forgot that I can say private in the module declaration.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Btw, is \AgdaHide predefined? I am just using %if false but this looks nicer.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Can you share your modification of agda.sty?<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Cheers,<u></u><u></u></span></p>
<p class="MsoNormal"><span>Thorsten <u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(181,196,223);padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Larrytheliquid <<a href="mailto:larrytheliquid@gmail.com" target="_blank">larrytheliquid@gmail.com</a>><br>
<b>Date: </b>Sunday, 2 August 2020 at 14:38<br>
<b>To: </b>Thorsten Altenkirch <<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>><br>
<b>Cc: </b>"<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Shadowing definitions<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Hi Thorsten,<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">I handled this in my thesis with modules as suggested, for example see `generic` getting repeated here:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><a href="https://github.com/larrytheliquid/thesis/blob/master/paper/Thesis/AST.lagda#L386-L422" target="_blank">https://github.com/larrytheliquid/thesis/blob/master/paper/Thesis/AST.lagda#L386-L422</a><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Note for nested modules you need to indent your code, which makes the output also contain<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">indented code because I `AgdaHide` the module declaration. It's definitely a hack, but because<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">I consistently use this style I modified `agda.sty` to always negative indent 2 spaces so the resulting<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">code always looks top-level.<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Sun, Aug 2, 2020 at 9:05 AM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-top:none;border-right:none;border-bottom:none;border-left:1pt solid rgb(204,204,204);padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">Thanks for the tip.<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">This works but usually the 2<sup>nd</sup> definition is a slight modification of the first. E.g. first I show how constructors can be derived and then I mention that one can use
the constructor keyword…<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Thorsten<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(181,196,223);padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From:
</span></b><span style="font-size:12pt;color:black">Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>><br>
<b>Date: </b>Sunday, 2 August 2020 at 13:59<br>
<b>To: </b>Thorsten Altenkirch <<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>><br>
<b>Cc: </b>"<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Shadowing definitions</span><u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Thorsten, would the following trick work? Go well, -- P<u></u><u></u></p>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">\definemacro{\mydef}{<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">\begin{code}<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">answer = 42<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">\end{code}<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">... first use of definition ...<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">\mydef<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">... second use of same definition ...<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">\mydef<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><br clear="all">
<u></u><u></u></p>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">. / \ and Senior Research Fellow, IOHK<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">.
<a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a><u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"> <u></u><u></u></p>
<div>
<div>
<p class="MsoNormal">On Sun, 2 Aug 2020 at 13:16, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-top:none;border-right:none;border-bottom:none;border-left:1pt solid rgb(204,204,204);padding:0cm 0cm 0cm 6pt;margin:5pt 0cm 5pt 4.8pt">
<div>
<div>
<p class="MsoNormal">Hi guys,<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">I am currently working on my book “The Tao of Types” and I am now using literate agda and lhs2tex with agda mode . One issue is that for pedagogical reasons I like to repeat definitions
but agda doesn’t allow this. Ok, I can declare the first definition as a spec which means it is ingnored by literate agda. I don’t really like this because it means that there is no type checking for the first definition. Also in some cases this doesn’t work
and I have to go through all sort of tricks to make the code work. Is there a workaround, or would it be possible to allow shadowing (unsafely)?<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Btw, another problem I have is to switch between agda-mode and latex-mode in emacs. I discovered that C-C C-n in latex mode switches to agda mode (not sure why) is there a key combination
to switch from agda to latex? <u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Cheers,<u></u><u></u></p>
<p class="MsoNormal">Thorsten<u></u><u></u></p>
</div>
<pre>This message and any attachment are intended solely for the addressee<u></u><u></u></pre>
<pre>and may contain confidential information. If you have received this<u></u><u></u></pre>
<pre>message in error, please contact the sender and delete the email and<u></u><u></u></pre>
<pre>attachment. <u></u><u></u></pre>
<pre> <u></u><u></u></pre>
<pre>Any views or opinions expressed by the author of this email do not<u></u><u></u></pre>
<pre>necessarily reflect the views of the University of Nottingham. Email<u></u><u></u></pre>
<pre>communications with the University of Nottingham may be monitored <u></u><u></u></pre>
<pre>where permitted by law.<u></u><u></u></pre>
<pre> <u></u><u></u></pre>
<pre> <u></u><u></u></pre>
<pre> <u></u><u></u></pre>
</div>
<p class="MsoNormal">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
</blockquote>
</div>
</div>
<pre>This message and any attachment are intended solely for the addressee<u></u><u></u></pre>
<pre>and may contain confidential information. If you have received this<u></u><u></u></pre>
<pre>message in error, please contact the sender and delete the email and<u></u><u></u></pre>
<pre>attachment. <u></u><u></u></pre>
<pre><u></u> <u></u></pre>
<pre>Any views or opinions expressed by the author of this email do not<u></u><u></u></pre>
<pre>necessarily reflect the views of the University of Nottingham. Email<u></u><u></u></pre>
<pre>communications with the University of Nottingham may be monitored <u></u><u></u></pre>
<pre>where permitted by law.<u></u><u></u></pre>
<pre><u></u> <u></u></pre>
<pre><u></u> <u></u></pre>
<pre><u></u> <u></u></pre>
</div>
<p class="MsoNormal">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal"><br clear="all">
<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">-- <u></u><u></u></p>
<div>
<p class="MsoNormal">Respectfully,<br>
Larry Diehl<u></u><u></u></p>
</div>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</pre></div>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature">Respectfully,<br>Larry Diehl<br></div>