David Thrane Christiansen

pie-hs. An implementation of Pie in Haskell

idris-type-providers. Type provider library for Idris

idris-quickcheck. A port of QuickCheck to Idris

epigram1. A version of Epigram 1 that can run with newer GHCs

IdrisAtGalois2015. Slides and exercises for the Idris course taught at Galois

IdrisSqlite. Effectful bindings for SQLite (forked from IdrisWeb)

final-pretty-printer. A monadic (and pretty) pretty printer for Haskell

pudding-old. A language-integrated proof assistant, for and in Racket

todo-list. A TODO list feature for DrRacket, like to Agda's goal list but for any language.

derive-all-the-instances. Work on type class deriving with elaboration reflection

idris-interaction.rkt. A Racket library for interacting with Idris over the IDE protocol

ssft24. Lean

racket-zippers. A zipper library for Racket

itu-thesis. A highly unofficial, still experimental LaTeX document class for ITU M.Sc. and Ph.D. theses and dissertations

tt-playground. A playground for type theory implementations in Racket

bob24. Lean

dr-racket-like-unicode. A clone of DrRacket-style Unicode symbol input for Emacs

dan-scheme. A very little language

idris-code-highlighter. A semantic highlighter for Idris code

prop-menu-el. Compute pop-up menus from text and overlay properties

idris-utils. Various Idris utility libraries. No guarantees. Some may end up in the stdlib someday, while others may be useless.

helm-idris. A Helm datasource for querying the Idris compiler

helm-pages. A Helm data source for pages in the current buffer

jonprl-mode. An Emac major mode for writing JonPRL code

Brainfun. A Brainf**k interpreter in Idris

pudding. Tactics in the macro expander

brush. A Racket literate programming system without tangling

lean-fkbh-24. Code examples from a Lean tutorial at the Copenhagen functional programming meetup

beamerOerestad. Unofficial IT University of Copenhagen beamer style

lean-fkbh-24-2. Example code used for presentation at F#unktionelle Københavnere, 2024-09-24

ghc-imported-from-el. Emacs support for Carlo Hamalainen's ghc-imported-from

racket-presentation-gui. Prototype implementation of presentation-based UI widgets for Racket's GUI library

annotated-wl-pprint. A variant of the Wadler-Leijen pretty-printer that allows arbitrary semantic annotations

Idris-dev. A Dependently Typed Functional Programming Language

helm-ghc. Helm support for ghc-mod metadata

iu-pict. A Racket pict for the IU logo