I'm curious why this syntax was adopted: `return z...

# arrow

[mikehearn]

I'm curious why this syntax was adopted: return z.post({ it > 0 }) { "greater than 0" } where the string is in a block, rather than a parameter. It seems less visually noisy to write as z.post("greater than zero") { it > 0 } - yeah it's different to require, but it seems to make more sense

[Alejandro Serrano Mena]

this is mostly to follow the syntax for Kotlin’s own require blocks

[Alejandro Serrano Mena]

https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/require.html

[stojan]

the main benefit is that the lambda is lazily evaluated, so no allocation happens unless the condition is broken

[mikehearn]

That's true for require but isn't true here, right? I thought pre/post are just hints to the SMT solver, they don't actually get compiled into the production code?

[mikehearn]

The string has to be a constant anyway?

[Alejandro Serrano Mena]

currently it does if you want it to be considered by Arrow Analysis

[Alejandro Serrano Mena]

indeed having the string inside { } is not needed for Analysis, but we still decided to do so for consistency