summaryrefslogtreecommitdiff
path: root/Test/wishlist/naked-function-in-recursive-setting.dfy.expect
blob: 4b1691b46c519c37b3f637d5f3b998c3744ab017 (plain)
1
2
3
4
5
6
7
8
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