Welcome! We notice you're using an outdated browser, which will result in a degraded experience on this site. Please consider a modern, fully supported browser.

webbureaucrat

The articles are just window-dressing for code snippets I want to keep.

Tagged “totality”

  1. Idris FizzBuzz Part I: Monads, Comments, and assert_smaller

    idris monad totality

    My journey of learning the Idris programming language continues! This article will start a tutorial series detailing how to write FizzBuzz in Idris. As before, my goal is to write without the assumption that all Idris learners already know Haskell. We will start by implementing modulo in Idris, and toward that goal we will go painfully slow because frankly this stuff is hard.

  2. Hello, Idris World! and Why I'm Excited for a Total Programming Language

    idris totality

    This article represents my first attempt to get up and running with the Idris programming language. It will document not only how to make an executable Idris package but also the basics of what Idris is and why it's not like any other programming language you're likely to have used before. From a practical perspective, it will cover some basic syntax as well as how to compile and run an Idris 2 program, including .ipkg usage.

See all tags.