Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
effects: make
:terminates_globally
functional on recursive functions
As with loop, it's hard to prove termination of recursive call automatically. But with this commit we can manually specify termination at least. ```julia Base.@assume_effects :terminates_globally function recur_termination1(x) x == 1 && return 1 1 < x < 20 || throw("bad") return x * recur_termination1(x-1) end @test fully_eliminated() do recur_termination1(12) end Base.@assume_effects :terminates_globally function recur_termination2(x) x == 1 && return 1 1 < x < 20 || throw("bad") return _recur_termination2(x) end _recur_termination2(x) = x * recur_termination2(x-1) @test fully_eliminated() do recur_termination2(12) end ```
- Loading branch information