naked-function-in-recursive-setting.dfy(4,9): Info: decreases n naked-function-in-recursive-setting.dfy(10,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 (0,0): anon7_Else (0,0): anon8_Else Dafny program verifier finished with 0 verified, 1 error