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

[ ambiguity ] rename `Concat.empty` in chapter "Interfaces" to something else

Open stefan-hoeck opened this issue 1 year ago • 0 comments

Recently, using the name empty has led to strange disambiguation bugs, probably due to a conflict with empty from Alternative.

stefan-hoeck avatar Mar 28 '23 07:03 stefan-hoeck