[Agda] Shadowing definitions

[Larrytheliquid]

Hi Thorsten,

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:
https://github.com/larrytheliquid/thesis/blob/master/paper/agda.sty
https://github.com/larrytheliquid/thesis/blob/master/paper/psu-thesis.sty
https://github.com/larrytheliquid/thesis/blob/master/paper/thesis.tex

However, it looks like the newest agda.sty has more configuration options
than it did years ago:
https://github.com/agda/agda/blob/master/src/data/agda.sty

For example, it might be enough to turn off the initial space around code:
\AgdaNoSpaceAroundCode
There's more config options and commands related to this but I'm unfamiliar
with them.

Also, it looks like AgdaHide still exists (
https://github.com/agda/agda/blob/master/src/data/agda.sty#L339-L343)
but is deprecated in favor of begin{code}[hide]

On Sun, Aug 2, 2020 at 11:39 AM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Hi Larry,
>
>
>
> Thank you for your email. Yes, this sounds like a good idea. Ok I forgot
> that I can say private in the module declaration.
>
>
>
> Btw, is \AgdaHide predefined? I am just using %if false but this looks
> nicer.
>
>
>
> Can you share your modification of agda.sty?
>
>
>
> Cheers,
>
> Thorsten
>
>
>
> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Larrytheliquid
> <larrytheliquid at gmail.com>
> *Date: *Sunday, 2 August 2020 at 14:38
> *To: *Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
> *Cc: *"agda at lists.chalmers.se" <agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Shadowing definitions
>
>
>
> Hi Thorsten,
>
>
>
> I handled this in my thesis with modules as suggested, for example see
> `generic` getting repeated here:
>
>
> https://github.com/larrytheliquid/thesis/blob/master/paper/Thesis/AST.lagda#L386-L422
>
>
>
> Note for nested modules you need to indent your code, which makes the
> output also contain
>
> indented code because I `AgdaHide` the module declaration. It's definitely
> a hack, but because
>
> I consistently use this style I modified `agda.sty` to always negative
> indent 2 spaces so the resulting
>
> code always looks top-level.
>
>
>
> On Sun, Aug 2, 2020 at 9:05 AM Thorsten Altenkirch <
> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
> Thanks for the tip.
>
>
>
> This works but usually the 2nd 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…
>
>
>
> Thorsten
>
>
>
> *From: *Philip Wadler <wadler at inf.ed.ac.uk>
> *Date: *Sunday, 2 August 2020 at 13:59
> *To: *Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
> *Cc: *"agda at lists.chalmers.se" <agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Shadowing definitions
>
>
>
> Thorsten, would the following trick work? Go well, -- P
>
>
>
> \definemacro{\mydef}{
>
> \begin{code}
>
> answer = 42
>
> \end{code}
>
>
>
> ... first use of definition ...
>
> \mydef
>
> ... second use of same definition ...
>
> \mydef
>
>
>
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
>
> .  /  \ and Senior Research Fellow, IOHK
>
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
>
>
>
>
>
> On Sun, 2 Aug 2020 at 13:16, Thorsten Altenkirch <
> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
> Hi guys,
>
>
>
> 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)?
>
>
>
> 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?
>
>
>
> Cheers,
>
> Thorsten
>
> 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.
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
> 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.
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> --
>
> Respectfully,
> Larry Diehl
>
> 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.
>
>
>
>
>

-- 
Respectfully,
Larry Diehl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200802/77bffacc/attachment.html>