Comment by lioeters

Oh how interesting, they're using a fork of Agda called Mikan, not Lean as I imagined before visiting the link. https://1lab.dev/Mikan.html