Есть ли примеры кода Agda, работающего в производстве?

Agda - хороший язык программирования для изучения зависимых типов и игры с интуиционистской теорией типов, а также для экспериментов с реализацией этих вещей. Но есть ли уже примеры "реальных" программ, написанных на Agda? Может быть, даже примеры, демонстрирующие его возможности (подобно тому, как xmonad часто упоминается как пример "настоящей" программы на Haskell)?