tutorial-code
tutorial-code copied to clipboard
Arguments of +-comm should be implicit
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 somewhere how the signature of a definition should be chosen (which arguments should be made implicit and which explicit).