agda/test/LaTeXAndHTML/succeed/TrailingColon.lagda.rst

Queso!

aaa

..
  ::
    module TrailingColon where

        data Bool : Set where
            true : Bool
            false : Bool
            aa : Bool

        a : Bool
        a = true

Tomate
bleh
bli

::
        b : Bool
        b = false


for example::

        c : Bool
        c = aa

and that's all, folks