On 06/04/17 13:08, Lars Hupel wrote:
>> Did you encounter an actual problem from that situation?
>>
>> Formally, a comment is not a problem. "Fixing" such things prematurely
>> is likely to break it.
>
> Yes, there is an actual problem. I define a function via
> "Function.add_function" and
> Your proposed change
> https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks
> formally OK.
See now Isabelle/3c628937899d and AFP/a7160ffc25f1.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
> A very weird error has somehow appeared
That was due to my change in inductive. It's all resolved now.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On 06/04/17 09:29, Lars Hupel wrote:
> while poking around in the function package (to store more information
> in "info"), I also realized that I need a little bit more information
> from the inductive package.
>
> Reading its sources, I stumbled upon 10-year-old comments by Makarius
> that
> Did you encounter an actual problem from that situation?
>
> Formally, a comment is not a problem. "Fixing" such things prematurely
> is likely to break it.
Yes, there is an actual problem. I define a function via
"Function.add_function" and inspect the resulting info. As per usual
discipline
Dear list,
while poking around in the function package (to store more information
in "info"), I also realized that I need a little bit more information
from the inductive package.
Reading its sources, I stumbled upon 10-year-old comments by Makarius
that remind the reader of (what I assume is)
