No longer allow hiding functions from the Dafny prelude by using hide *. This affected recursive functions because they use $LS which is defined in the prelude.
How has this been tested?
Added a CLI test-case to revealFunctions.dfy
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Fixes #5763
Description
hide *
. This affected recursive functions because they use$LS
which is defined in the prelude.How has this been tested?
revealFunctions.dfy
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.