lane

Modular Group as a mutual inductive type

15

This is a construction of the Modular Group PSL2(Z) utilizing a mutual inductive type. I will quote from the preamble of the Type declaration to contextualize the formalization presented here....

Natural Order definition utilizing an identity type

4

Quoting from the preamble: ``` Following the equality case of the triangle inequality, we can define a partial order on ℕ directly with an identity type, namely by considering the...

Vimscript: is this a design choice?

9

Hi, I've recently picked up Cornelis and I'm enamored thinking about the possibilities of how the vim ecosystem could assist Agda programming, as its a great foundation. I use neovim...