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, and this may discourage the new user from Arend. Is is better to introduce tactics gradually one-by-one throughout the 1st Part of the tutorial (the way it is done in Coq tutorials for example) rather than devote a separate lesson to them.
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, and this may discourage the new user from Arend. Is is better to introduce tactics gradually one-by-one throughout the 1st Part of the tutorial (the way it is done in Coq tutorials for example) rather than devote a separate lesson to them.