<!-- This file was automatically generated by agda2lagda 0.2023.6.9. -->

Sample non-literate Agda program
================================

A remark to test bulleted lists:

* This file serves as example for agda2lagda.

* The content may be non-sensical.

Indeed!

```agda
module Foo where
```

Some data type.

```agda
data D : Set where
  c : D
```

A function.

```agda
foo : D → D
foo c = c   -- basically, the identity
```

<!-- This part is commented out.
{-
bar : D → Set
bar x = D
-- -}
--
 -->
A subheading
-------------

```agda
module Submodule where

  postulate
    zeta : D
```

That's it.
Bye.