In viper we can use `decreases` to prove termination. We currently do not support this, we would need this to show functions like fibonacci. It would be great to add this feature to SnaKt. [Viper decreases documentation](https://viper.ethz.ch/tutorial/termination-measures.html)
In viper we can use
decreasesto prove termination. We currently do not support this, we would need this to show functions like fibonacci.It would be great to add this feature to SnaKt.
Viper decreases documentation