[Merged by Bors] - feat: to_additive
#234
Conversation
A memoised fixpoint function.
List.length_map was added to core and the arguments are the other way around.
|
Is there still some meaning to the draft status of this PR (given that you've remove the WIP label)? |
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
The current status of this PR is that it is feature complete and I can get most examples to work, however there are still things to do:
|
…ult. I don't understand what I changed to cause this
|
It might be a good idea to merge this sooner rather than when it is at feature parity and bug free. I think the bugs and features that we really need will become apparent once porting is underway. |
| match ← tryCatch (m *> pure none) (pure ∘ some) with | ||
| | none => throwError "Expected an exception." | ||
| | some ex => return ex |
There was a problem hiding this comment.
I wonder if this is clearer:
| match ← tryCatch (m *> pure none) (pure ∘ some) with | |
| | none => throwError "Expected an exception." | |
| | some ex => return ex | |
| try | |
| discard m | |
| throwError "Expected an exception." | |
| catch ex => | |
| return ex |
There was a problem hiding this comment.
hmm I think this doesn't quite work because it needs to throw if m doesn't throw
| @@ -64,11 +64,11 @@ is rewritten to: op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ) | |||
| when (↑(↑(x : α) : β) : γ) = (↑(x : α) : γ) can be proven with a squash lemma | |||
| -/ | |||
| def splittingProcedure (expr : Expr) : MetaM Simp.Result := do | |||
| let Expr.app (Expr.app op x ..) y .. := expr | return {expr} | |||
| let Expr.app (Expr.app op x ..) y .. := expr | return {expr := expr} | |||
There was a problem hiding this comment.
We really need to figure out something to disambiguate the set and record notations.
I completely agree. bors d+ |
|
✌️ EdAyers can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
By @fpvandoorn. Depends on #129 Closes #229 Co-authored-by: E.W.Ayers <edward.ayers@outlook.com>
|
Pull request successfully merged into master. Build succeeded: |
By @fpvandoorn.
Depends on #129
Closes #229