david-christiansen/pudding-old

Stars
40
Rank 680,660 (Top 14 %)
Language
Racket
License
GNU Lesser Genera...
Created almost 9 years ago
Updated over 8 years ago

david-christiansen/pudding-old

david-christiansen

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

A language-integrated proof assistant, for and in Racket

pie-hs

An implementation of Pie in Haskell

idris-type-providers

Type provider library for Idris

idris-quickcheck

A port of QuickCheck to Idris

IdrisAtGalois2015

Slides and exercises for the Idris course taught at Galois

epigram1

A version of Epigram 1 that can run with newer GHCs

IdrisSqlite

Effectful bindings for SQLite (forked from IdrisWeb)

final-pretty-printer

A monadic (and pretty) pretty printer for Haskell

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

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

racket-zippers

A zipper library for Racket

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

bob24

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

tiny-dependent-types

A very simple implementation of a little dependently typed language

prop-menu-el

Compute pop-up menus from text and overlay properties

helm-pages

A Helm data source for pages in the current buffer

jonprl-mode

An Emac major mode for writing JonPRL code

pudding

Tactics in the macro expander

Brainfun

A Brainf**k interpreter in Idris

brush

A Racket literate programming system without tangling

annotated-wl-pprint

A variant of the Wadler-Leijen pretty-printer that allows arbitrary semantic annotations

racket-presentation-gui

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

narrowed-page-navigation

An Emacs package for showing a buffer page-by-page, intended for presentations and live coding.

ghc-imported-from-el

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

helm-ghc

Helm support for ghc-mod metadata

live-code-talks

An Emacs package to highlight special comments for in-buffer slide-shows.

idris-tf-random

A port of the Haskell tf-random to Idris

barcodes-code128

A Haskell library for generating Code 128 barcodes

scala-doc-search

A Hoogle clone for Scaladoc

iu-pict

A Racket pict for the IU logo

pretty-examples

Examples of our PP lib

emacs-old-norse-input

An Old Norse input method for Emacs

racket-abt

An ABT library for Racket

simple-relational-refinement

frank.el

Emacs mode for the Frank language

typesearch

idris-raytracer

Unfinished raytracer in Idris for use in testing compiler optimizations

dynamic-haskell-ffi

Experimentation with dynamically loading C libraries from Haskell (learning exercise)

lean-fkbh-24

Code examples from a Lean tutorial at the Copenhagen functional programming meetup

ssft24