chore: Fix code in README.md + (auto)align version in repl + minor improvements (typos, etc.)
#36
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
duesee
commented
Jan 10, 2025
| @@ -37,7 +37,7 @@ Loaded! | |||
|
|
|||
| We can then ask it to solve 2 + 3 (and find the correct answer 5): | |||
|
|
|||
| ``` | |||
| ```text | |||
There was a problem hiding this comment.
This PR makes it so that README.md is used in lib.rs as Rust doc (see below) to check the code. Rust assumes code blocks to be "rust" by default, so we need to say "text" here.
duesee
commented
Jan 10, 2025
| We can now ask the solver to prove statements within this universe, e.g. that "there exists an X | ||
| such that X + 2 = 3". This statement is indeed true for X = 1, and indeed, the solver will provide | ||
| this answer: | ||
| // We can now ask the solver to prove statements within this universe, e.g. that "there exists an X |
There was a problem hiding this comment.
The easiest way to make cargo test pass was to merge these blocks. We are trading flexibility of writing for correctness, though.
duesee
commented
Jan 10, 2025
| @@ -147,6 +147,11 @@ | |||
| //! | |||
| //! | |||
|
|
|||
| // Test examples from README.md. | |||
There was a problem hiding this comment.
This "trick" allows to ensure the code in the README.md is checked during cargo test w/o using additional dependencies.
duesee
commented
Jan 10, 2025
| @@ -131,8 +139,7 @@ r.insert(Rule::fact(is_natural, vec![z.into()])); | |||
| // Define the rule `is_natural(s(P)) :- is_natural(P)`, i.e. that | |||
| // the successor of P is a natural number if P is also a natural number. | |||
| r.insert(ast::forall(|[p]| { | |||
| Rule::fact(is_natural, vec![ast::app(s, vec![p.into()])]) | |||
| .when(is_natural, vec![p.into()]) | |||
| Rule::fact(is_natural, vec![ast::app(s, vec![p.into()])]).when(is_natural, vec![p.into()]) | |||
There was a problem hiding this comment.
This is due to rustfmt.
duesee
commented
Jan 10, 2025
| // Obtain an iterator that allows us to exhaustively search the solution space: | ||
| let solutions = query_dfs( | ||
| &r, | ||
| &mut r, |
There was a problem hiding this comment.
This and the following makes cargo test pass. Not sure if it's the best way to resolve.
fatho
approved these changes
Jan 20, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I think the title says everything. I'll add a bit of explanation inline.
PS: Thanks for this library! We are looking very closely into it, because it might help us a lot!