Writing Agda blog posts in literate markdown

Posted by Jesper on March 19, 2019

This is a super fancy blog post written in literate Agda!

open import Agda.Builtin.Nat

this : Nat  Nat
this zero = {!!}
this (suc x) = {!!}