-
Notifications
You must be signed in to change notification settings - Fork 35
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
Coq export for symbol with definition defined with tactics #1057
Comments
Hi Alessio. The exports to Coq are purely syntactic currently: they are done after parsing and before elaboration. So they do not handle proofs (I should update the doc). For this reason, they are very efficient. I see 2 solutions to overcome this problem:
|
What do you consider the easiest to do in a short time?
The Lambdapi tactic is very similar to the Coq tactic so it should be a direct translation no? I am interested in developing this feature. My goal is to be able to export my SMT proof in Coq 😄. PS: Maybe the person in charge of Vodk in your team is interested in this feature? |
The translation of tactics should be very easy to experiment (you just need to add a few lines in export/coq.ml). If it works, it will be interesting as it will keep the translation very efficient (linear in the size of files). But it may be the case that the semantics of lambdapi and coq tactics are slightly different, in which case you would need to define coq tactics implementing lambdapi ones. |
Hi,
I would like to export in Coq format symbol that has been defined with tactics like the symbol
test_export2
below:But when I run the command
lambdapi export -v 0 -o stt_coq Test.lp
I get the error:
The text was updated successfully, but these errors were encountered: