feat: allow slim_check to do work in MetaM #3838
Open
+114
−79
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
added 5 commits
May 7, 2023 22:54
semorrison
added
the
merge-conflict
semorrison
removed
the
merge-conflict
semorrison
added
the
merge-conflict
semorrison
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
eric-wieser
reviewed
Jul 19, 2023
|
|
||
| /-- `Random α` gives us machinery to generate values of type `α` -/ | ||
| class Random (α : Type u) where | ||
| random [RandomGen g] : RandG g α | ||
| random [RandomGen g] : RandG g Id α |
There was a problem hiding this comment.
Is there a reason these don't generalize across monads m?
There was a problem hiding this comment.
Because I couldn't get it to work.
eric-wieser
reviewed
Jul 19, 2023
|
|
||
| namespace Rand | ||
| /-- Generate one more `Nat` -/ | ||
| def next [RandomGen g] : RandG g Nat := do | ||
| def next [RandomGen g] : RandG g Id Nat := do |
There was a problem hiding this comment.
Suggested change
| def next [RandomGen g] : RandG g Id Nat := do | |
| def next [RandomGen g] [Monad m] : RandG g m Nat := do |
or is there a reason not to?
eric-wieser
reviewed
Jul 19, 2023
Comment on lines
+151
to
+152
| instance : MonadLift (Rand m) m where | ||
| monadLift := runRand |
There was a problem hiding this comment.
This strikes me as a bit risky; I'd rather not accidentally run a random monad with the default generator and get something less deterministic than expecfted.
leanprover-community-mathlib4-bot
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
bors
bot
changed the base branch from
master
to
ScottCarnahan/BinomialRing2
semorrison
changed the base branch from
ScottCarnahan/BinomialRing2
to
master
|
@semorrison what's the status of this PR? If you'd still like this to be reviewed, could you resolve the merge conflicts |
joneugster
added
awaiting-author
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.
This opens the possibility to e.g. run
norm_numinside aTestableinstance.Ideally we would actually add a
Testableinstance that demonstrates this. :-)Some hurdles:
norm_numcan't decide all equalities in the reals. Does it just respond withsuccessif it can't decide? We could add an extra case toTestResultcalledinconclusive, but I think the code paths would be the same as forsuccess.MetaDecidable, for propositions with decision procedures inMetaM. There would be a lot of new design there.slim_check.