Definition 1.2.2.  We define:
⊤ := [true]