Follow
nothing can stop me from making extremely unfunny jokes about how the inductive-inductive version of [something] is called [something]-[something].
@amy writing some recursive-recursive functions i see
@amy the termination-termination checker will stop you
@agdakx Not a fan of Eliminating-eliminating higher pattern-pattern matching? 🥲
oh yeah the constructor-constructors. the case-case tree