Sergey Sinchuk
Sergey Sinchuk
To be able show that the `StateMonad` is a monad, you need to be able to prove equality of two instances of classes. Even I only know that this can...
When a problem is formulated about `gcd` or matrices, it would be nice to explain the reader how he could check their answer. The students whom I assigned solving these...
It would be nice to explain how the user can connect `arend-lib` to the tutorial code. Explain in accessible way the format of a `arend.yaml` files. What is the difference...
It would be nice to include some material about the very basics of tactics in the tutorial. For example, rewrite/rewriteI/at/I/unfold/ext. Their absence leads to too much verbosity when solving exercises,...
To be able solve one of the exercises in 6th lesson (namely the exercise about `Maybe` monad), you need to know what a dependent `\case` is, and this is explained...
The `+-comm` in `EqualityProofs` must have arguments `n` `m` implicit (because that's the standard pattern actually used in `arend-lib` and everywhere else in the tutorial). Maybe you need to explain...
Some definitions given in the tutorial have differently defined counterparts with the same name from `arend-lib`. 1. in the tutorial `||` is the non-truncated definition, but in `arend-lib` it is...
``` \instance FreeMonoidConstr (S : \Set) : Monoid \cowith | E => List S | ide => nil | * (a1 : List S) (a2 : List S) => a1...
``` com.intellij.diagnostic.PluginException: PSI element is provided on EDT by com.intellij.ui.popup.PopupListAdapter$MyListWrapper.getData("selectedItem"). Please move that to a BGT data provider using PlatformCoreDataKeys.BGT_DATA_PROVIDER at com.intellij.diagnostic.PluginProblemReporterImpl.createPluginExceptionByClass(PluginProblemReporterImpl.java:23) at com.intellij.diagnostic.PluginException.createByClass(PluginException.java:90) at com.intellij.ide.impl.DataValidators.reportPsiElementOnEdt(DataValidators.java:96) at com.intellij.ide.impl.DataValidators.isDataValid(DataValidators.java:71) at com.intellij.ide.impl.DataValidators.validOrNull(DataValidators.java:64)...
If the user forgets to surround mcases tactic with parentheses he won't get an error message. Instead he will get "missing clauses" message (despite the fact that clauses are present...