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.

Sign up for GitHub

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

Jump to bottom

UR: proof states are not updated after proving new conjectures! #186

Open
yutakang opened this issue Jun 5, 2021 · 3 comments
Open

UR: proof states are not updated after proving new conjectures! #186

yutakang opened this issue Jun 5, 2021 · 3 comments
Assignees
@yutakang
Labels
bug

Comments

@yutakang
Copy link
Collaborator

yutakang commented Jun 5, 2021

In the current implementation, proof states are not updated after proving new conjectures!

Therefore, subsequent proof attempts are unable to take advantage of such proved conjectures.

This needs to be fixed.
@yutakang yutakang added the bug label Jun 5, 2021
@yutakang yutakang self-assigned this Jun 5, 2021
@yutakang
Copy link
Collaborator Author

yutakang commented Jun 5, 2021

Probably I can do something similar to what I did in Australia for Cogent.

@yutakang
Copy link
Collaborator Author

yutakang commented Jun 5, 2021

That is, use Local_Theory.note (a, ths).

@yutakang
Copy link
Collaborator Author

yutakang commented Jun 5, 2021

I have to use Proof.theorem to update Proof.state using Local_Theory.note as is done in this code.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@yutakang yutakang

Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@yutakang