[Agda] Shadowing definitions

[Philip Wadler]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200802/845c4d1d/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200802/845c4d1d/attachment.ksh>