nunchaku on continuous functions on codatatypes in Isabelle

[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.

[blanchette]

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 ***@***.***> 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 <#34?email_source=notifications&email_token=AAFZTYZXTQ7CUDDFYHHVIKLQE2WHDA5CNFSM4IMHWDW2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HFU55BQ>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAFZTYZLFZTGRGNVLXOQQC3QE2WHDANCNFSM4IMHWDWQ>.

[singhjagadish]

Hello,

the lemmas I have tested nunchaku on are at the bottom of the theory.

Thanks,
Jagadish

Codatatype.zip

[blanchette]

Dear Jagadish, Just to tell you that I'm not forgetting the issue, but I will be on vacation the next two weeks and won't be able to look into this until after then. Cheers, Jasmin

…

On 19 Aug 2019, at 18:11, singhjagadish ***@***.***> wrote: Hello, the lemmas I have tested nunchaku on are at the bottom of the theory. Thanks, Jagadish Codatatype.zip <https://github.com/nunchaku-inria/nunchaku/files/3516640/Codatatype.zip> — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#34?email_source=notifications&email_token=AAFZTY33QLVALPO7L6ZMRFDQFLA3PA5CNFSM4IMHWDW2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD4TPHVQ#issuecomment-522646486>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAFZTY3NH6JCBEYFCOJZ2FDQFLA3PANCNFSM4IMHWDWQ>.