blanchette
commented
5 years ago Hello,
Could you send me a complete self-contained Isabelle example that triggers this behavior?
Thanks,
Jasmin
On 16 Aug 2019, at 15:51, singhjagadish notifications@github.com wrote:
Hello,
I have another question about the Isabelle plugin. Maybe you can answer it, even though the plugin is not ready yet, or @blanchette https://github.com/blanchette if he is currently working on the plugin.
While testing nunchaku on a codatatype, I found out that it doesn't work on continuous functions (or functions which use continuous functions). Instead, it gives the following error: Error: env: undefined ID 'anon_fun_7' (code 1). We looked for possible ways to define ID in the documentation (in this section: https://nunchaku-inria.github.io/nunchaku/0.6/nunchaku/Nunchaku_core/Env/index.html <x-msg://11/url>) and, unfortunately, didn't have any idea how to do it. Maybe you know if that was the right approach, or what we may actually have to do in order to make nunchaku work for continuous function.
Thank you in advance.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/nunchaku-inria/nunchaku/issues/34?email_source=notifications&email_token=AAFZTYZXTQ7CUDDFYHHVIKLQE2WHDA5CNFSM4IMHWDW2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HFU55BQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AAFZTYZLFZTGRGNVLXOQQC3QE2WHDANCNFSM4IMHWDWQ.
singhjagadish
Hello,
I have another question about the Isabelle plugin. Maybe you can answer it, even though the plugin is not ready yet, or @blanchette if he is currently working on the plugin.
While testing nunchaku on a codatatype, I found out that it doesn't work on continuous functions (or functions which use continuous functions). Instead, it gives the following error:
Error: env: undefined ID 'anon_fun_7' (code 1). We looked for possible ways to define ID in the documentation (in this section: https://nunchaku-inria.github.io/nunchaku/0.6/nunchaku/Nunchaku_core/Env/index.html) and, unfortunately, didn't have any idea how to do it. Maybe you know if that was the right approach, or what we may actually have to do in order to make nunchaku work for continuous function.Thank you in advance.