Iverson bracket

Let $𝑝$ be a decidable proposition. The Iverson bracket is defined as follows #m/def/general

[𝑝] = {1 𝑝 0 \neg 𝑝

This is a generalization of the Kronecker delta.

#state/tidy | #lang/en | #SemBr