a "let function" without postcondition should not generate any VC
If one defines a "let function" with an empty contract, like in
let function pi : real = 3.1416
then there is a VC (requiring to prove true
) to prove. This is a annoying useless noise
Could we avoid that ?