Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Can't find nun-file after using nunchaku in isabelle #33

Open
singhjagadish opened this issue Jun 21, 2019 · 1 comment
Open

Can't find nun-file after using nunchaku in isabelle #33

singhjagadish opened this issue Jun 21, 2019 · 1 comment
Labels
isabelle-plugin related to Isabelle

Comments

@singhjagadish
Copy link

Hello,

I have used nunchaku on an isabelle lemma, and I get an error because of an ill-formed term (probably caused by using an own datatype, more specifically a domain). It also shows the directory where the .nun-file (nunchaku2832584.nun) of the process should be.
However, I couldn't find the file there, so my question is how to get the information of the file, as it could be helpful for using nunchaku for such a datatype.

Thanks in advance.

@c-cube
Copy link
Member

c-cube commented Jun 26, 2019

The nunchaku plugin is Isabelle isn't production ready yet, sorry. @blanchette would probably know more but he's quite busy these days.

@c-cube c-cube added the isabelle-plugin related to Isabelle label Jun 26, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
isabelle-plugin related to Isabelle
Projects
None yet
Development

No branches or pull requests

2 participants