tutorial-code icon indicating copy to clipboard operation
tutorial-code copied to clipboard

Arguments of +-comm should be implicit

Open sxhya opened this issue 1 year ago • 0 comments

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).

sxhya avatar Mar 22 '23 19:03 sxhya