[Agda] Shadowing definitions

[Larrytheliquid]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200802/aa9a05c7/attachment.html>