Fix function name in one of the erasure examples#4911

hyphenrf wants to merge 1 commit intoidris-lang:masteridris-lang/Idris-dev:masterfrom

hyphenrf:patch-1hyphenrf/Idris-dev:patch-1Copy head branch name to clipboard