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

API changes #41

Merged
merged 7 commits into from
Oct 18, 2021
Merged

API changes #41

merged 7 commits into from
Oct 18, 2021

Conversation

tirix
Copy link
Collaborator

@tirix tirix commented Oct 17, 2021

  • added accessors to information requiring parse_result(), which is not public anymore,
  • added a Frame reference, with iterators on essential and floating formulas,
  • append_to_stack_buffer is needed as an external API, to build proofs,
  • added an iterator over all statements of the database, which was otherwise not accessible anymore,
  • added an implementation of Debug for FormulaRef
  • fixed a few comments

@tirix tirix requested a review from digama0 October 17, 2021 13:55
src/database.rs Outdated Show resolved Hide resolved
src/formula.rs Outdated Show resolved Hide resolved
src/scopeck.rs Outdated Show resolved Hide resolved
src/scopeck.rs Outdated Show resolved Hide resolved
src/scopeck.rs Outdated Show resolved Hide resolved
tirix and others added 3 commits October 18, 2021 11:25
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@tirix tirix merged commit 73a94aa into metamath:main Oct 18, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants