Skip to content



@leastfixed @dpndnt


  1. Agda formalisation of NbE for λ□

    Agda 16

  2. Notes for my talk

    Agda 1

  3. Total functional programming (ESFP) literature

    181 10

  4. Charity language interpreters and literature

    C 99 3

  5. ET (IPL) language interpreters and literature

    Standard ML 28 1

  6. idris-bash Archived

    GNU bash backend for Idris

    Haskell 56 3

167 contributions in the last year

Oct Nov Dec Jan Feb Mar Apr May Jun Jul Aug Sep Oct Mon Wed Fri

Contribution activity

October 2020

mietek has no activity yet for this period.

September 2020

Created an issue in agda/agda that received 9 comments

`mutual` blocks should be functionally equivalent to new-style implicit mutual recursion

I don’t think I’m the only one who finds mutual blocks to be more readable than new-style implicit mutual recursion. Unfortunately, mutual blocks s…


Seeing something unexpected? Take a look at the GitHub profile guide.

You can’t perform that action at this time.