add coq-stdpp as dependency, add abs_examples module #12
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.
Let's add Std++ as a dependency so we get access to the nice
by
finisher and other nice stuff.by
is used to guarantee that a goal is properly discharged and applies some heuristics likeauto
.This should be easy for you to rebase over, right @Aqissiaq?
I will do a followup PR later where I add arithmetic and boolean expressions and some more examples of typing proofs.