Documentation differentiation - #2053
Open
yosakaon wants to merge 8 commits into
Open
Conversation
Comment on lines
+67
to
+72
| (* `Lemma is_derive_example (W : normedModType R) *) | ||
| (* (t : R^o) (f g : R^o -> W) (f' g' : W) v : *) | ||
| (* is_derive t v f f' -> *) | ||
| (* is_derive t v g g' -> *) | ||
| (* is_derive t v (f + g) (f' + g'). *) | ||
| (* Proof. move => is_der_f is_der_g. by apply: is_derive_eq. Qed.` *) |
Member
There was a problem hiding this comment.
It is maybe better to put this piece of code between triple backquotes.
Comment on lines
+80
to
+88
| (* Hypothesis derivable_f : forall t, derivable f t 1. *) | ||
| (* Hypothesis derivable_h : forall t, derivable h t 1. *) | ||
| (* Local Instance is_derive_f t : is_derive t 1 f ('D_1 f t). *) | ||
| (* by apply: derivableP. Qed. *) | ||
| (* Local Instance is_derive_h t : is_derive t 1 h ('D_1 h t). *) | ||
| (* by apply: derivableP. Qed. *) | ||
| (* *) | ||
| (* Lemma is_derivable_example (t : R^o) : derivable (f+h) t 1. *) | ||
| (* Proof. apply/ex_derive. Qed. *) |
Member
There was a problem hiding this comment.
Maybe better inside a pair of triple backquotes.
| (* To verify the value of a given function you can apply `derive_val` or *) | ||
| (* diff_val`, given the right `is_derive/diff` instances are defined such as :*) | ||
| (* *) | ||
| (* Lemma is_derive_val_example t : *) |
Member
There was a problem hiding this comment.
Same here about triple backquotes.
affeldt-aist
requested changes
Jul 28, 2026
affeldt-aist
left a comment
affeldt-aist
left a comment
Member
There was a problem hiding this comment.
Many thanks for writing this done!
Member
|
Note that you can check the automatically generated documentation of this PR by downloading the artifact produced by the CI job |
Contributor
Author
It seems like the CI fails before generating documentation |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Motivation for this change
This PR fixes #1996 and #1839, in particular the use of
is_diffandis_deriveChecklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers