david-christiansen/idris-type-providers david-christiansen/idris-type-providers

  • Stars
    star
    85
  • Rank 385,668 (Top 8 %)
  • Language Idris
  • Created over 11 years ago
  • Updated almost 7 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
david-christiansen/idris-type-providers
github

david-christiansen

Reviews

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

Repository Details

Type provider library for Idris

More Repositories

1

pie-hs

An implementation of Pie in Haskell
Haskell
189
star
2

idris-quickcheck

A port of QuickCheck to Idris
Idris
57
star
3

IdrisAtGalois2015

Slides and exercises for the Idris course taught at Galois
Idris
50
star
4

epigram1

A version of Epigram 1 that can run with newer GHCs
Haskell
49
star
5

IdrisSqlite

Effectful bindings for SQLite (forked from IdrisWeb)
Idris
40
star
6

pudding-old

A language-integrated proof assistant, for and in Racket
Racket
40
star
7

final-pretty-printer

A monadic (and pretty) pretty printer for Haskell
Haskell
34
star
8

todo-list

A TODO list feature for DrRacket, like to Agda's goal list but for any language.
Racket
33
star
9

derive-all-the-instances

Work on type class deriving with elaboration reflection
Idris
31
star
10

idris-interaction.rkt

A Racket library for interacting with Idris over the IDE protocol
Racket
30
star
11

itu-thesis

A highly unofficial, still experimental LaTeX document class for ITU M.Sc. and Ph.D. theses and dissertations
TeX
20
star
12

tt-playground

A playground for type theory implementations in Racket
Racket
20
star
13

racket-zippers

A zipper library for Racket
Racket
19
star
14

dr-racket-like-unicode

A clone of DrRacket-style Unicode symbol input for Emacs
Emacs Lisp
17
star
15

dan-scheme

A very little language
Racket
15
star
16

idris-code-highlighter

A semantic highlighter for Idris code
Idris
14
star
17

bob24

Lean
12
star
18

idris-utils

Various Idris utility libraries. No guarantees. Some may end up in the stdlib someday, while others may be useless.
Idris
11
star
19

helm-idris

A Helm datasource for querying the Idris compiler
Emacs Lisp
10
star
20

tiny-dependent-types

A very simple implementation of a little dependently typed language
F#
10
star
21

prop-menu-el

Compute pop-up menus from text and overlay properties
Emacs Lisp
10
star
22

helm-pages

A Helm data source for pages in the current buffer
Emacs Lisp
10
star
23

jonprl-mode

An Emac major mode for writing JonPRL code
Emacs Lisp
8
star
24

pudding

Tactics in the macro expander
Racket
6
star
25

Brainfun

A Brainf**k interpreter in Idris
Idris
6
star
26

brush

A Racket literate programming system without tangling
Racket
6
star
27

annotated-wl-pprint

A variant of the Wadler-Leijen pretty-printer that allows arbitrary semantic annotations
Haskell
4
star
28

racket-presentation-gui

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

narrowed-page-navigation

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

ghc-imported-from-el

Emacs support for Carlo Hamalainen's ghc-imported-from
Emacs Lisp
4
star
31

helm-ghc

Helm support for ghc-mod metadata
Emacs Lisp
4
star
32

live-code-talks

An Emacs package to highlight special comments for in-buffer slide-shows.
Emacs Lisp
4
star
33

idris-tf-random

A port of the Haskell tf-random to Idris
C
3
star
34

barcodes-code128

A Haskell library for generating Code 128 barcodes
Haskell
3
star
35

scala-doc-search

A Hoogle clone for Scaladoc
Scala
3
star
36

iu-pict

A Racket pict for the IU logo
Racket
3
star
37

pretty-examples

Examples of our PP lib
Haskell
2
star
38

emacs-old-norse-input

An Old Norse input method for Emacs
Emacs Lisp
2
star
39

racket-abt

An ABT library for Racket
Racket
2
star
40

simple-relational-refinement

Haskell
1
star
41

frank.el

Emacs mode for the Frank language
Emacs Lisp
1
star
42

typesearch

Scala
1
star
43

idris-raytracer

Unfinished raytracer in Idris for use in testing compiler optimizations
1
star
44

dynamic-haskell-ffi

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

lean-fkbh-24

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

ssft24

Lean
1
star