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 “idris”

  1. Idris FizzBuzz Part IV: Main and .ipkg Files

    idris nixos

    This is the fourth and final part of a walkthrough of FizzBuzz, a common interview problem, in Idris. If you haven't read the other parts, you can start with Part I. To show how to import and use libraries, we're going to divide this project into a library and an executable. Along the way, we will create .ipkg packages for both.

  2. Idris FizzBuzz Part III: Defining Types and Importing Modules

    idris variant

    This is Part III of my attempt to explain how to use the Idris programming language through a tutorial on FizzBuzz, the common software development hiring interview problem. If you're new to Idris and haven't read Part I and Part II, I recommend doing that now. This article will go over defining our own types and importing our own modules as well as recap what we've learned about case-matching and basic syntax.

  3. Idris FizzBuzz Part II: Maybes, Infix Notation, and Idris Holes

    idris monad

    Let's conntinue on our journey of writing FizzBuzz in the Idris programming language. If you haven't already, I encourage you to read Part I for an introduction to the problem as well as some basic syntax, and, importantly, information on totality checking.

  4. 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.

  5. 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.