## This is a most popular repository list for Idris sorted by number of stars
|STARS|FORKS|ISSUES|LAST COMMIT|NAME/PLACE|DESCRIPTION|
| --- | --- | --- | --- | --- | --- |
| 930 | 66 | 79 | 10 months ago | [Idris2-boot](https://github.com/edwinb/Idris2-boot)/1 | A dependently typed programming language, a successor to Idris |
| 546 | 38 | 8 | 1 year, 11 months ago | [Blodwen](https://github.com/edwinb/Blodwen)/2 | A prototype successor to Idris |
| 397 | 26 | 15 | 2 years ago | [software-foundations](https://github.com/idris-hackers/software-foundations)/3 | Software Foundations in Idris |
| 343 | 16 | 55 | 1 year, 6 days ago | [typedefs](https://github.com/typedefs/typedefs)/4 | Programming language agnostic type construction language based on polynomials. |
| 319 | 17 | 10 | 12 hours ago | [idris-jvm](https://github.com/mmhelloworld/idris-jvm)/5 | JVM bytecode back end for Idris |
| 311 | 19 | 1 | 1 year, 4 months ago | [awesome-idris](https://github.com/joaomilho/awesome-idris)/6 | 𝛌 Awesome Idris resources |
| 225 | 45 | 10 | 2 years ago | [lightyear](https://github.com/ziman/lightyear)/7 | Parser combinators for Idris |
| 210 | 18 | 27 | 1 year, 2 months ago | [idris-ct](https://github.com/statebox/idris-ct)/8 | formally verified category theory library |
| 196 | 11 | 8 | 6 years ago | [iridium](https://github.com/puffnfresh/iridium)/9 | xmonad with the X11 abstracted and configured with Idris |
| 184 | 13 | 4 | 4 years ago | [idris-demos](https://github.com/idris-hackers/idris-demos)/10 | Collection of Idris tests and demonstration programs |
| 170 | 24 | 1 | 7 years ago | [idris-koans](https://github.com/idris-hackers/idris-koans)/11 | Koans are small lessons on the path to enlightenment. The aim of the Idris Koans project is to provide an easy learning environment in Idris. Your insight will be derived by encountering failing code and fixing them so that they type check. |
| 146 | 11 | 1 | 2 years ago | [quantities](https://github.com/timjb/quantities)/12 | Type-safe physical computations and unit conversions in Idris ⚖ 🌡 ⏲ 🔋 📐 |
| 145 | 37 | 9 | 4 years ago | [TypeDD-Samples](https://github.com/edwinb/TypeDD-Samples)/13 | Sample code from "Type Driven Development with Idris" |
| 119 | 12 | 0 | 3 years ago | [idris2048](https://github.com/KesterTong/idris2048)/14 | 2048 in Idris |
| 117 | 12 | 3 | 3 years ago | [idris-crypto](https://github.com/idris-hackers/idris-crypto)/15 | Implementation of cryptographic primitives using Idris |
| 110 | 2 | 0 | 2 years ago | [hezarfen](https://github.com/joom/hezarfen)/16 | a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features |
| 92 | 22 | 1 | 1 year, 1 month ago | [idris-containers](https://github.com/jfdm/idris-containers)/17 | Various data structures for use in the Idris Language. |
| 86 | 11 | 3 | 3 years ago | [IdrisScript](https://github.com/idris-hackers/IdrisScript)/18 | FFI Bindings to interact with the unsafe world of JavaScript |
| 84 | 10 | 10 | 1 year, 1 month ago | [idris-tparsec](https://github.com/gallais/idris-tparsec)/19 | TParsec - Total Parser Combinators in Idris |
| 82 | 20 | 2 | 10 months ago | [SPLV20](https://github.com/edwinb/SPLV20)/20 | SPLV20 course notes |
| 79 | 6 | 2 | 5 years ago | [idris-type-providers](https://github.com/david-christiansen/idris-type-providers)/21 | Type provider library for Idris |
| 61 | 5 | 2 | 2 years ago | [recursion_schemes](https://github.com/vmchale/recursion_schemes)/22 | Recursion schemes for Idris |
| 57 | 14 | 5 | a day ago | [idris2-lsp](https://github.com/idris-community/idris2-lsp)/23 | Language Server for Idris2 |
| 56 | 8 | 2 | 6 years ago | [IdrisNet2](https://github.com/SimonJF/IdrisNet2)/24 | A proper network library for Idris, now that I know what I'm doing. |
| 55 | 9 | 2 | 7 years ago | [idris-quickcheck](https://github.com/david-christiansen/idris-quickcheck)/25 | A port of QuickCheck to Idris |
| 53 | 10 | 1 | 2 years ago | [specdris](https://github.com/pheymann/specdris)/26 | A test framework for Idris |
| 50 | 3 | 3 | 1 year, 2 months ago | [idris-grin](https://github.com/grin-compiler/idris-grin)/27 | GRIN backend for Idris |
| 50 | 2 | 0 | 4 years ago | [IdrisUnityPlayground](https://github.com/bamboo/IdrisUnityPlayground)/28 | Experiments in Idris / Unity integration. |
| 50 | 5 | 3 | 1 year, 8 days ago | [fsm-oracle](https://github.com/statebox/fsm-oracle)/29 | Finite state machines as graphs |
| 49 | 0 | 0 | 5 years ago | [IdrisAtGalois2015](https://github.com/david-christiansen/IdrisAtGalois2015)/30 | Slides and exercises for the Idris course taught at Galois |
| 49 | 12 | 1 | 6 years ago | [idris101](https://github.com/ToJans/idris101)/31 | Learning project by a group of people interested in learning the Idris language |
| 47 | 19 | 14 | 4 years ago | [SDL-idris](https://github.com/edwinb/SDL-idris)/32 | SDL bindings package for idris |
| 46 | 6 | 0 | 1 year, 4 months ago | [idrisjs](https://github.com/rbarreiro/idrisjs)/33 | Js libraries for idris |
| 44 | 6 | 1 | 13 hours ago | [idris2-elab-util](https://github.com/stefan-hoeck/idris2-elab-util)/34 | Utilities and documentation for exploring idirs2's new elaborator reflection. |
| 41 | 5 | 2 | 3 years ago | [idris-cs-hse](https://github.com/bravit/idris-cs-hse)/35 | «Функциональное программирование с зависимыми типами на языке Idris» — мини-курс на ФКН ВШЭ |
| 40 | 11 | 3 | 6 years ago | [iQuery](https://github.com/idris-hackers/iQuery)/36 | Idris Lib to interact with the DOM and Browser API for the JavaScript backend |
| 39 | 2 | 0 | 6 years ago | [blog](https://github.com/bmsherman/blog)/37 | None |
| 39 | 4 | 0 | 6 years ago | [bam-idris-blog](https://github.com/puffnfresh/bam-idris-blog)/38 | Static blog generator in Idris. |
| 38 | 6 | 1 | 2 years ago | [differentiable-idris](https://github.com/doofin/differentiable-idris)/39 | dependent types meets deep learning |
| 38 | 1 | 0 | 3 years ago | [LICK](https://github.com/i-am-tom/LICK)/40 | Idris-written, correct-by-construction, simply-typed lambda calculus. |
| 36 | 3 | 0 | 4 years ago | [States](https://github.com/edwinb/States)/41 | State machines in Idris |
| 36 | 3 | 0 | 2 years ago | [Todo](https://github.com/leon-vv/Todo)/42 | Idris Todo web application example |
| 36 | 8 | 3 | 5 years ago | [IdrisSqlite](https://github.com/david-christiansen/IdrisSqlite)/43 | Effectful bindings for SQLite (forked from IdrisWeb) |
| 35 | 5 | 9 | 3 years ago | [idris-bi](https://github.com/sbp/idris-bi)/44 | Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq |
| 35 | 7 | 2 | 2 years ago | [idris-http](https://github.com/uwap/idris-http)/45 | An HTTP library for idris |
| 35 | 3 | 1 | 3 years ago | [IdrisPipes](https://github.com/QuentinDuval/IdrisPipes)/46 | A library for composable and effectful production, transformation and consumption of streams of data in Idris |
| 32 | 8 | 2 | 3 years ago | [idris-posix](https://github.com/idris-hackers/idris-posix)/47 | System POSIX bindings for Idris. |
| 32 | 3 | 0 | 5 years ago | [WS-idr](https://github.com/edwinb/WS-idr)/48 | Yes, it is what you think it is |
| 32 | 3 | 2 | 2 years ago | [ikan](https://github.com/idris-industry/ikan)/49 | build tool and package manager for idris,in idris,with free monads |
| 31 | 5 | 4 | 2 years ago | [derive-all-the-instances](https://github.com/david-christiansen/derive-all-the-instances)/50 | Work on type class deriving with elaboration reflection |
| 31 | 0 | 0 | 3 years ago | [IdrisReducers](https://github.com/QuentinDuval/IdrisReducers)/51 | Transducers for Idris: a library for composable algorithmic transformation. |
| 31 | 4 | 0 | 7 days ago | [idris2dart](https://github.com/bamboo/idris2dart)/52 | The Dart backend for Idris 2. |
| 30 | 0 | 1 | a month ago | [pearl-binary-search](https://github.com/gallais/pearl-binary-search)/53 | Functional Pearl: Certified Binary Search in a Read-Only Array |
| 30 | 1 | 0 | 1 year, 10 months ago | [icfp-bingo-2017-idris](https://github.com/gergoerdi/icfp-bingo-2017-idris)/54 | ICFP Bingo 2017 (Idris edition) |
| 29 | 0 | 0 | 2 months ago | [code](https://github.com/sequents/code)/55 | Proof theory seminar |
| 29 | 3 | 4 | 4 years ago | [totalscript](https://github.com/totalscript/totalscript)/56 | Explore what a powerful type system can do. |
| 29 | 3 | 1 | 9 months ago | [permutations](https://github.com/vmchale/permutations)/57 | Provides a type-safe way of working with permutations in Idris |
| 29 | 4 | 3 | 5 years ago | [probability](https://github.com/fieldstrength/probability)/58 | Probabilistic computation in Idris |
| 29 | 0 | 0 | 2 years ago | [sequent-calc-talk](https://github.com/clayrat/sequent-calc-talk)/59 | Code for the "Logic, machines and sequent calculus" talk  |
| 28 | 2 | 1 | 3 days ago | [idrall](https://github.com/alexhumphreys/idrall)/60 | Dhall bindings for Idris |
| 26 | 7 | 3 | 4 years ago | [idris-protobuf](https://github.com/google/idris-protobuf)/61 | A partial implementation of Protocol Buffers in Idris |
| 26 | 15 | 30 | 2 hours ago | [idris](https://github.com/exercism/idris)/62 | Exercism exercises in Idris. |
| 26 | 4 | 0 | 2 months ago | [idris-insertion-sort](https://github.com/davidfstr/idris-insertion-sort)/63 | Provably correct implementation of insertion sort in Idris. |
| 25 | 2 | 0 | 4 years ago | [flying-spaghetti-monster](https://github.com/ctford/flying-spaghetti-monster)/64 | An Idris type provider for communicating type-checkable protocols. |
| 24 | 9 | 5 | 3 years ago | [idris-free](https://github.com/idris-hackers/idris-free)/65 | Free Monads and useful constructions to work with them |
| 24 | 0 | 0 | 3 years ago | [idris-but-its-c](https://github.com/LightAndLight/idris-but-its-c)/66 | Idris, but it's C |
| 23 | 2 | 1 | 5 years ago | [examples](https://github.com/vindaloo-thesis/examples)/67 | Code samples inspiring language design |
| 23 | 1 | 0 | 6 years ago | [tarts](https://github.com/japesinator/tarts)/68 | Timing attack resistant type systems |
| 23 | 0 | 1 | 1 year, 4 months ago | [IdrisApp](https://github.com/edwinb/IdrisApp)/69 | An extensible IO-like monad-like thing for Idris, with support for including linear subprograms |
| 23 | 5 | 1 | 7 years ago | [idris-cph-exercises](https://github.com/idris-hackers/idris-cph-exercises)/70 | Exercises from the Idris lecture series presented at the ITU Copenhagen on March 11--15, updated to work with latest Idris releases. |
| 23 | 0 | 0 | 1 year, 4 months ago | [idris-cam](https://github.com/thautwarm/idris-cam)/71 | Sucessor: https://github.com/thautwarm/Quick-Backend |
| 22 | 1 | 0 | 6 months ago | [idris-sesh](https://github.com/wenkokke/idris-sesh)/72 | Session types in Idris2! |
| 22 | 0 | 0 | 3 years ago | [Iaia](https://github.com/sellout/Iaia)/73 | A recursion scheme library for Idris. |
| 22 | 4 | 4 | 4 years ago | [idris-lens](https://github.com/idris-hackers/idris-lens)/74 | None |
| 21 | 1 | 3 | 3 months ago | [sequent-calc](https://github.com/clayrat/sequent-calc)/75 | Experiments with sequent calculi |
| 21 | 1 | 0 | 4 years ago | [tdd-with-idris](https://github.com/steshaw/tdd-with-idris)/76 | Working through Type-Driven Development with Idris |
| 21 | 1 | 0 | 2 years ago | [smproc](https://github.com/jameshaydon/smproc)/77 | A well-typed symmetric-monoidal category of concurrent processes |
| 21 | 1 | 10 | 2 years ago | [gloss-idris](https://github.com/thalerjonathan/gloss-idris)/78 | A port of the gloss library from Haskell to Idris |
| 20 | 1 | 0 | 2 years ago | [Idris-HoTT](https://github.com/jaredloomis/Idris-HoTT)/79 | Homotopy Type Theory proofs in Idris |
| 20 | 1 | 7 | 7 months ago | [idris-patricia](https://github.com/kowainik/idris-patricia)/80 | 🌋 Idris implementation of patricia tree |
| 20 | 4 | 4 | 6 hours ago | [idris-frex](https://github.com/frex-project/idris-frex)/81 | None |
| 20 | 8 | 1 | 3 years ago | [idris-lens](https://github.com/HuwCampbell/idris-lens)/82 | van Laarhoven lenses for Idris |
| 20 | 0 | 0 | a month ago | [Idris2-Effect](https://github.com/Russoul/Idris2-Effect)/83 | Experimental effects library for Idris 2 |
| 20 | 1 | 2 | 1 year, 1 month ago | [rekenaar](https://github.com/jdevuyst/rekenaar)/84 | Idris tactics for (commutative) monoids |
| 19 | 3 | 0 | 17 days ago | [extensible-records](https://github.com/gonzaw/extensible-records)/85 | Extensible records for Idris |
| 19 | 7 | 1 | 4 years ago | [idris-config](https://github.com/jfdm/idris-config)/86 | Parsers for various configuration files written in Idris. |
| 19 | 0 | 1 | 1 year, 11 months ago | [fizzbuzz-i](https://github.com/0xd34df00d/fizzbuzz-i)/87 | FizzBuzz, formally verified, provably correct |
| 18 | 1 | 1 | 7 years ago | [IdrisObjCExperiment](https://github.com/andyarvanitis/IdrisObjCExperiment)/88 | None |
| 18 | 9 | 2 | 5 years ago | [idris-algebra](https://github.com/idris-hackers/idris-algebra)/89 | This is an attempt at painting as many bikesheds as possible with a typeclass hierarchy for idris reflecting "Algebra" |
| 18 | 2 | 1 | 7 years ago | [bibdris](https://github.com/ziman/bibdris)/90 | BibTeX database management in Idris |
| 18 | 1 | 0 | 5 days ago | [Idris2-Grin](https://github.com/Z-snails/Idris2-Grin)/91 | GRIN backend for Idris2 |
| 18 | 4 | 1 | 6 years ago | [Verified](https://github.com/reynir/Verified)/92 | A collection of proofs for some idris class instances - NOT MAINTAINED |
| 18 | 8 | 3 | 4 years ago | [Idris-Bifunctors](https://github.com/japesinator/Idris-Bifunctors)/93 | A small bifunctor library for idris |
| 18 | 4 | 2 | 2 years ago | [RingIdris](https://github.com/FranckS/RingIdris)/94 | Ring solver for Idris |
| 17 | 3 | 0 | 15 days ago | [idris-snippets](https://github.com/palladin/idris-snippets)/95 | Collection of Idris snippets |
| 17 | 2 | 1 | 2 years ago | [categories](https://github.com/danilkolikov/categories)/96 | Category Theory |
| 17 | 1 | 0 | 8 months ago | [Idris2-Ocaml](https://github.com/karroffel/Idris2-Ocaml)/97 | OCaml backend for Idris2 |
| 17 | 1 | 1 | 11 months ago | [game-idris](https://github.com/corazza/game-idris)/98 | A game in Idris |
| 17 | 0 | 0 | 10 days ago | [sae](https://github.com/DoctorRyner/sae)/99 | An Idris 2 build tool and a package manager |
| 16 | 1 | 0 | 3 years ago | [FarRP](https://github.com/lambda-11235/FarRP)/100 | An arrowized FRP library for Idris with static safety guarantees. |
| 16 | 2 | 0 | 6 years ago | [fp-in-idris](https://github.com/domdere/fp-in-idris)/101 | Functional Programing in Scala (in Idris) [Idris] |
| 15 | 2 | 0 | 2 months ago | [idris-refined](https://github.com/janschultecom/idris-refined)/102 | Port of Scala/Haskell Refined library to Idris |
| 15 | 0 | 0 | 4 months ago | [itt-idris](https://github.com/ziman/itt-idris)/103 | ITT: quantified dependent calculus with inference of all modalities, implemented in Idris 2 |
| 15 | 1 | 0 | 6 months ago | [aoc-2020-idris](https://github.com/JoeyEremondi/aoc-2020-idris)/104 | My Idris2 solutions/attempts for Advent of Code 2020 |
| 15 | 0 | 34 | 2 years ago | [elemental-magicks](https://github.com/programminglanguagesclub/elemental-magicks)/105 | Idris + Ur/Web development of a perfect information, fair, deterministic turn based strategy game, built with dependent types! |
| 15 | 1 | 0 | 2 years ago | [tm-proposer-idris](https://github.com/cwgoes/tm-proposer-idris)/106 | Formalization of Tendermint proposer election properties |
| 15 | 1 | 0 | 3 years ago | [idris-dict](https://github.com/be5invis/idris-dict)/107 | A Dict k v in Idris |
| 15 | 0 | 0 | a month ago | [Idris2-Lua](https://github.com/Russoul/Idris2-Lua)/108 | Lua backend for Idris 2 |
| 14 | 0 | 0 | 3 years ago | [univalence-from-scratch](https://github.com/jdolson/univalence-from-scratch)/109 | Univalence from scratch in Idris |
| 14 | 1 | 1 | a day ago | [idris2-sop](https://github.com/stefan-hoeck/idris2-sop)/110 | Idris port of Haskell's sop-core library |
| 14 | 0 | 0 | 2 days ago | [idris2-clibs](https://github.com/edwinb/idris2-clibs)/111 | Idris 2 bindings to various C libraries |
| 14 | 4 | 1 | 4 years ago | [Idris-Profunctors](https://github.com/japesinator/Idris-Profunctors)/112 | A small profunctor library for idris |
| 14 | 0 | 0 | 4 years ago | [gpif-idris](https://github.com/pbl64k/gpif-idris)/113 | Translation of Agda code in A. Löh and J. P. Magalhães *Generic Programming with Indexed Functors* to Idris. |
| 14 | 2 | 0 | 5 years ago | [Idris](https://github.com/mukeshtiwari/Idris)/114 | Codes related to Idris |
| 14 | 3 | 7 | 3 years ago | [idris-code-highlighter](https://github.com/david-christiansen/idris-code-highlighter)/115 | A semantic highlighter for Idris code |
| 14 | 2 | 0 | 6 years ago | [Idris-WebGL](https://github.com/MaxOw/Idris-WebGL)/116 | WebGL bindings for Idris. |
| 13 | 1 | 0 | 6 years ago | [stl-idris](https://github.com/puffnfresh/stl-idris)/117 | Code from my StrangeLoop 2014 Idris presentation. |
| 13 | 3 | 1 | 5 years ago | [text](https://github.com/ziman/text)/118 | Text framework for Idris |
| 13 | 2 | 1 | 6 years ago | [idris-pong](https://github.com/trillioneyes/idris-pong)/119 | A browser Pong game, taking advantage of Idris's ability to compile to javascript. |
| 13 | 1 | 0 | 7 years ago | [Eff-new](https://github.com/edwinb/Eff-new)/120 | New version of Effects library with dependent states |
| 13 | 1 | 0 | 1 year, 11 months ago | [dependable-data-structures](https://github.com/jdevuyst/dependable-data-structures)/121 | Experiments in implementing functional data structures in Idris |
| 13 | 1 | 0 | 4 months ago | [idris2-curl](https://github.com/MarcelineVQ/idris2-curl)/122 | libcurl bindings for idris2 |
| 13 | 0 | 0 | 2 years ago | [ttstar](https://github.com/ziman/ttstar)/123 | Dependently typed core calculus with erasure |
| 13 | 2 | 0 | 1 year, 1 month ago | [idris-xml](https://github.com/jfdm/idris-xml)/124 | A simple XML module for Idris. |
| 13 | 1 | 0 | 6 months ago | [idris2-streaming](https://github.com/MarcelineVQ/idris2-streaming)/125 | Effectful Streaming for Idris |
| 13 | 4 | 1 | 2 years ago | [curses-idris](https://github.com/JakobBruenker/curses-idris)/126 | Curses bindings package for Idris |
| 13 | 1 | 0 | 2 years ago | [idris-elm](https://github.com/lagunoff/idris-elm)/127 | The Elm architecture ported to Idris Programming language |
| 13 | 0 | 0 | 8 months ago | [modal-types](https://github.com/clayrat/modal-types)/128 | Experiments with modal types |
| 13 | 0 | 0 | 2 years ago | [linear](https://github.com/vmchale/linear)/129 | Linear lenses in Blodwen |
| 13 | 0 | 0 | 7 years ago | [Idris-CPDT](https://github.com/sellout/Idris-CPDT)/130 | A translation of Certified Programming with Dependent Types to Idris. |
| 12 | 0 | 0 | 13 hours ago | [idris2-hedgehog](https://github.com/stefan-hoeck/idris2-hedgehog)/131 | An Idris port of the Haskell Hedghog library |
| 12 | 0 | 0 | 6 years ago | [xquant](https://github.com/fieldstrength/xquant)/132 | Dependently-typed structures for quantum physics in Idris |
| 12 | 7 | 1 | 4 years ago | [gl-idris](https://github.com/eckart/gl-idris)/133 | None |
| 12 | 2 | 0 | 3 years ago | [idris-graphql](https://github.com/jameshaydon/idris-graphql)/134 | Idris GraphQL |
| 12 | 0 | 0 | 3 years ago | [idris-linear](https://github.com/clayrat/idris-linear)/135 | Experiments with linear types  |
| 12 | 2 | 1 | 3 years ago | [idris-tmustache](https://github.com/gallais/idris-tmustache)/136 | Total Logic-Less Templating Library |
| 12 | 1 | 0 | 4 years ago | [SeqDecProbs](https://github.com/nicolabotta/SeqDecProbs)/137 | None |
| 12 | 6 | 0 | 1 year, 3 months ago | [http4idris](https://github.com/A1kmm/http4idris)/138 | An experimental HTTP framework for Idris |
| 12 | 2 | 1 | 6 years ago | [idris-ffi-example](https://github.com/idris-industry/idris-ffi-example)/139 | A minimal example of the Idris C FFI |
| 11 | 0 | 0 | 4 years ago | [idris-clean](https://github.com/timjs/idris-clean)/140 | A priliminary backend for Idris that compiles to Clean. |
| 11 | 2 | 0 | 3 years ago | [idris-benchmarks](https://github.com/ziman/idris-benchmarks)/141 | Some benchmarks for Idris |
| 11 | 0 | 0 | 3 years ago | [Idris-json](https://github.com/eraserhd/Idris-json)/142 | Formally verified JSON parser |
| 11 | 4 | 0 | 6 years ago | [idris-utils](https://github.com/david-christiansen/idris-utils)/143 | Various Idris utility libraries. No guarantees. Some may end up in the stdlib someday, while others may be useless. |
| 11 | 0 | 0 | 3 years ago | [UnionType](https://github.com/berewt/UnionType)/144 | UnionType in Idris |
| 10 | 7 | 5 | 4 years ago | [SDL2-idris](https://github.com/eckart/SDL2-idris)/145 | SDL2 Bindings for the Idris programming language |
| 10 | 0 | 1 | 3 years ago | [ivor](https://github.com/emptyflash/ivor)/146 | The steam powered Idris package manager |
| 10 | 0 | 2 | 9 months ago | [idris2-libgit2](https://github.com/bigs/idris2-libgit2)/147 | Libgit2 bindings for Idris 2 |
| 10 | 2 | 5 | 2 years ago | [desc-n-crunch](https://github.com/ahmadsalim/desc-n-crunch)/148 | Desc'n crunch: Descriptions, levitation, and reflecting the elaborator. |
| 10 | 8 | 2 | 3 years ago | [idris-bytes](https://github.com/ziman/idris-bytes)/149 | FFI-based byte buffers for Idris |
| 10 | 5 | 0 | 3 years ago | [Idris.Yaml](https://github.com/Heather/Idris.Yaml)/150 | Idris YAML lib |
| 10 | 2 | 4 | 19 hours ago | [REPLica](https://github.com/ReplicaTest/REPLica)/151 | Golden tests for command-line interfaces. |
| 10 | 2 | 0 | 7 years ago | [IdrisNet](https://github.com/SimonJF/IdrisNet)/152 | Verified networking using dependent types |
| 10 | 2 | 0 | 5 years ago | [idris-httpclient](https://github.com/justjoheinz/idris-httpclient)/153 | A http client for Idris based on libcurl |
| 10 | 2 | 1 | 2 months ago | [FeOFu](https://github.com/u235axe/FeOFu)/154 | Features of the Future |
| 10 | 3 | 0 | a month ago | [IdrisExtSTGCodegen](https://github.com/andorp/IdrisExtSTGCodegen)/155 | None |
| 9 | 0 | 10 | 3 years ago | [verified-integer-gaussian-elimination](https://github.com/runKleisli/verified-integer-gaussian-elimination)/156 | Idris package defining, implementing, and verifying naiive Gaussian elimination over the integers in some system of linear algebra. |
| 9 | 1 | 0 | 3 years ago | [idris-dimensions](https://github.com/writeoncereadmany/idris-dimensions)/157 | Dimensions library in Idris |
| 9 | 0 | 0 | 6 years ago | [31C3Slides](https://github.com/raichoo/31C3Slides)/158 | 31C3 Slides |
| 9 | 1 | 0 | 8 months ago | [typedtext.io](https://github.com/chrrasmussen/typedtext.io)/159 | None |
| 9 | 4 | 4 | 5 months ago | [jerrington.me](https://github.com/tsani/jerrington.me)/160 | Personal website |
| 9 | 0 | 1 | 6 years ago | [Records](https://github.com/jmars/Records)/161 | Dependently Typed Extensible Records with Prototypal Inheritance |
| 9 | 1 | 2 | 4 years ago | [idris-testing](https://github.com/jfdm/idris-testing)/162 | Testing Utilities for Idris programs. |
| 9 | 1 | 0 | 1 year, 9 months ago | [tlhydra](https://github.com/Termina1/tlhydra)/163 | Idris parser and serializer/deserealizer for TL language |
| 9 | 1 | 1 | 4 months ago | [idris2-elab-deriving](https://github.com/MarcelineVQ/idris2-elab-deriving)/164 | implementation deriving for idris2 |
| 9 | 1 | 2 | 6 years ago | [ConcIO](https://github.com/edwinb/ConcIO)/165 | Concurrent IO language with Uniqueness Types |
| 9 | 2 | 1 | 5 years ago | [idrisregexp](https://github.com/rodrigogribeiro/idrisregexp)/166 | Regular expression matching in Idris |
| 9 | 1 | 0 | 3 years ago | [idris-pfds](https://github.com/timjb/idris-pfds)/167 | Purely functional data structures in Idris |
| 9 | 0 | 0 | 5 years ago | [CId](https://github.com/TimRichter/CId)/168 | a little category theory in Idris |
| 9 | 3 | 0 | 5 years ago | [csd-utwente](https://github.com/bravit/csd-utwente)/169 | Certified Software Development with Dependent Types in Idris |
| 9 | 2 | 0 | 7 years ago | [idris-webgl](https://github.com/mankyKitty/idris-webgl)/170 | Experimentation with Idris and WebGL via JavaScript FFI |
| 9 | 0 | 0 | 6 days ago | [idris2-dom](https://github.com/stefan-hoeck/idris2-dom)/171 | Javascript DOM bindings for Idris2 |
| 8 | 1 | 0 | 2 years ago | [idris-regex](https://github.com/MathiasVP/idris-regex)/172 | Verified implementation of Brzozowski derivatives in Idris |
| 8 | 0 | 0 | 2 years ago | [idris-wasm](https://github.com/jDomantas/idris-wasm)/173 | None |
| 8 | 0 | 0 | 5 years ago | [strangegroup-idris-June2014](https://github.com/raichoo/strangegroup-idris-June2014)/174 | Code I presented in a demo at Strange Group |
| 8 | 0 | 0 | a month ago | [idris-data-frame](https://github.com/ziman/idris-data-frame)/175 | Data frames for Idris 2 |
| 8 | 0 | 0 | 5 months ago | [kweh](https://github.com/raptazure/kweh)/176 | A simple dependently typed language with unification |
| 8 | 0 | 0 | 3 years ago | [idris-libuv-example](https://github.com/brainrape/idris-libuv-example)/177 | code example for using Idris with a libuv-based async C runtime |
| 8 | 1 | 1 | 4 years ago | [idris-binary-rationals](https://github.com/mcgordonite/idris-binary-rationals)/178 | An idris rational number type built from paths in the Stern Brocot tree |
| 8 | 0 | 0 | 4 years ago | [idris-logic](https://github.com/yurrriq/idris-logic)/179 | Propositional logic tools, inspired by the Coq standard library. |
| 8 | 1 | 0 | 3 months ago | [responsible](https://github.com/brainrape/responsible)/180 | Idris 2 HTTP Api Server |
| 8 | 0 | 0 | 5 days ago | [lightclick](https://github.com/border-patrol/lightclick)/181 | LightClick is a linearly typed orchestration language for Systems-on-a-Chip Designs that supports lightweight dependent types in the form of domain-specific indexed-types. |
| 8 | 13 | 14 | 1 year, 3 months ago | [LTS2019](https://github.com/siddhartha-gadgil/LTS2019)/182 | Web page, code for "Logic, Types Spaces 2019" at IISc |
| 7 | 0 | 1 | 6 years ago | [idris-partiality](https://github.com/puffnfresh/idris-partiality)/183 | The partiality monad in Idris. |
| 7 | 0 | 0 | 4 years ago | [levitation](https://github.com/RyanGlScott/levitation)/184 | Following along with the paper "The Practical Guide to Levitation" by Ahmad Salim Al-Sibahi |
| 7 | 0 | 5 | 1 year, 9 months ago | [tp](https://github.com/superfunc/tp)/185 | Strongly Typed Paths for Idris |
| 7 | 0 | 0 | 3 years ago | [idris-electron](https://github.com/jheiling/idris-electron)/186 | Electron bindings for Idris |
| 7 | 0 | 0 | 5 years ago | [idris-fiamma](https://github.com/archaeron/idris-fiamma)/187 | Generate HTML from idris |
| 7 | 0 | 0 | 4 years ago | [dstbx](https://github.com/statebox/dstbx)/188 | dependently typed Statebox (heavy WIP) |
| 7 | 0 | 0 | 7 years ago | [khartes](https://github.com/dysinger/khartes)/189 | An Experiment with Both Haskell & Idris JS FFI interface to AWS |
| 7 | 0 | 0 | 1 year, 9 months ago | [blott-experiments](https://github.com/clayrat/blott-experiments)/190 | Experiments with dependent modal types |
| 7 | 2 | 0 | 3 years ago | [idris-argparse](https://github.com/jfdm/idris-argparse)/191 | A simple argument parser written in Idris. |
| 7 | 1 | 1 | 3 years ago | [pacman](https://github.com/jdublu10/pacman)/192 | A proof that Idris is pacman complete |
| 7 | 0 | 0 | 8 months ago | [idris2-mlf](https://github.com/ziman/idris2-mlf)/193 | Malfunction backend for Idris 2 |
| 7 | 0 | 0 | 4 months ago | [idris2-extras](https://github.com/mb64/idris2-extras)/194 | Some extra utilities for programming in Idris 2. |
| 7 | 2 | 0 | 5 years ago | [alacarte-idris](https://github.com/pa-ba/alacarte-idris)/195 | Data Types a la Carte in Idris |
| 6 | 1 | 1 | 4 years ago | [cairo-idris](https://github.com/eckart/cairo-idris)/196 | Idris Bindings for libcairo |
| 6 | 1 | 0 | 3 years ago | [idris-react](https://github.com/jheiling/idris-react)/197 | React bindings for Idris |
| 6 | 0 | 0 | 5 months ago | [TAPL-Idris](https://github.com/andylokandy/TAPL-Idris)/198 | None |
| 6 | 0 | 0 | a day ago | [idris2-json](https://github.com/stefan-hoeck/idris2-json)/199 | Automatically derivable JSON marshallers in the spirit of Haskell's aeson |
| 6 | 0 | 0 | 3 years ago | [idris-coda](https://github.com/ostera/idris-coda)/200 | 📦 A collection of Idris packages |
| 6 | 0 | 0 | 7 years ago | [idris-toys](https://github.com/trillioneyes/idris-toys)/201 | An eclectic collection of beginner Idris code |
| 6 | 1 | 0 | 1 year, 8 months ago | [idris-dataframe](https://github.com/argent0/idris-dataframe)/202 | Data structure inspired by R's data frames. |
| 6 | 0 | 0 | a month ago | [toml-idr](https://github.com/tiatomee/toml-idr)/203 | A TOML parser for Idris 2 |
| 6 | 0 | 0 | 6 years ago | [sfidris](https://github.com/GuglielmoS/sfidris)/204 | Examples and exercises of Software Foundations in Idris |
| 6 | 0 | 0 | 6 years ago | [idris-monadic-parser](https://github.com/tauli/idris-monadic-parser)/205 | None |
| 6 | 2 | 0 | 4 years ago | [idris-yampa](https://github.com/BartAdv/idris-yampa)/206 | Idris implementation of Yampa FRP library as described in Reactive Programming through Dependent Types. WIP |
| 6 | 2 | 4 | 3 years ago | [idris-vdom](https://github.com/brandondyck/idris-vdom)/207 | Virtual DOM in pure Idris |
| 6 | 1 | 0 | 6 years ago | [idris-commonmark](https://github.com/soimort/idris-commonmark)/208 | Idris wrapper for jgm's Markdown parser |
| 6 | 0 | 0 | 4 years ago | [IdrisBowlingKata](https://github.com/QuentinDuval/IdrisBowlingKata)/209 | A type safety challenge in Idris: encoding the rules of Bowling inside the type system |
| 6 | 0 | 0 | 6 years ago | [scott-encoding](https://github.com/mietek/scott-encoding)/210 | TODO |
| 6 | 0 | 3 | 3 years ago | [idr-logical-foundations](https://github.com/fabianhjr/idr-logical-foundations)/211 | Logical Foundations in Idris |
| 6 | 1 | 0 | 3 years ago | [battle](https://github.com/emccorson/battle)/212 | JavaScript battle game written in Idris |
| 6 | 0 | 0 | 11 months ago | [exp-subs](https://github.com/clayrat/exp-subs)/213 | Explicit substitution calculi |
| 6 | 0 | 0 | 18 days ago | [BiSH](https://github.com/Qeenon/BiSH)/214 | Idris 2 static web blog generator |
| 6 | 2 | 2 | 4 years ago | [idris-hamt](https://github.com/bamboo/idris-hamt)/215 | Idris Hash Array Mapped Trie |
| 6 | 1 | 0 | 6 years ago | [Brainfun](https://github.com/david-christiansen/Brainfun)/216 | A Brainf**k interpreter in Idris |
| 6 | 0 | 0 | 4 years ago | [wyvern](https://github.com/ericqweinstein/wyvern)/217 | A little web server written in Idris. |
| 6 | 1 | 0 | 3 years ago | [idris-sandbox](https://github.com/mbrodersen/idris-sandbox)/218 | Idris Sandbox |
| 6 | 0 | 0 | 5 years ago | [Oz](https://github.com/davidwlewis/Oz)/219 | Hardware Description Language embedded in Idris |
| 6 | 0 | 0 | 5 years ago | [ucph-msc-thesis-dpdt](https://github.com/cassiebaer/ucph-msc-thesis-dpdt)/220 | Masters Thesis - Differential Privacy + Dependent Types |
| 6 | 0 | 0 | 2 years ago | [cube.idr](https://github.com/aatxe/cube.idr)/221 | An implementation of the Lambda Cube in Idris. |
| 6 | 1 | 1 | 8 months ago | [idris2-bytes](https://github.com/MarcelineVQ/idris2-bytes)/222 | ByteStrings for Idris2! |
| 6 | 0 | 0 | 4 years ago | [spim-compiler](https://github.com/taktoa/spim-compiler)/223 | A compiler from a simple imperative language to SPIM, a dialect of MIPS assembly (WIP) |
| 6 | 1 | 0 | 2 years ago | [stoorts](https://github.com/appositum/stoorts)/224 |  stoorts little aquele rato branco la do filme |
| 6 | 1 | 4 | 2 years ago | [idris-multihash](https://github.com/statebox/idris-multihash)/225 | Multihash for Idris |
| 6 | 5 | 2 | 4 years ago | [idris-array](https://github.com/idris-hackers/idris-array)/226 | primitive flat arrays containing Idris values |
| 6 | 1 | 1 | 2 years ago | [Control.Eternal.Idris](https://github.com/Heather/Control.Eternal.Idris)/227 | tiny idris library |
| 5 | 0 | 0 | 6 years ago | [IdrisCSVExample](https://github.com/raichoo/IdrisCSVExample)/228 | CSV Example using Type Providers |
| 5 | 2 | 0 | 5 years ago | [idris-hangman](https://github.com/eeue56/idris-hangman)/229 | Example of hangman in Idris |
| 5 | 0 | 0 | 4 years ago | [tap-idris](https://github.com/ostera/tap-idris)/230 | :beers: A simple TAP producer and consumer/reporter for Idris |
| 5 | 3 | 2 | 4 years ago | [the-power-of-pi](https://github.com/yurrriq/the-power-of-pi)/231 | Implementations of ideas in The Power of Pi. |
| 5 | 1 | 0 | 6 years ago | [brainfuck-idris](https://github.com/gergoerdi/brainfuck-idris)/232 | Brainfuck interpreter in Idris |
| 5 | 0 | 0 | 4 months ago | [log-rels](https://github.com/clayrat/log-rels)/233 | Logical relations and normalisation |
| 5 | 5 | 3 | 10 months ago | [optparse-idris](https://github.com/HuwCampbell/optparse-idris)/234 | Minimal port of optparse-applicative to idris |
| 5 | 0 | 0 | 3 years ago | [idris-microKanren](https://github.com/joom/idris-microKanren)/235 | Simple microKanren implementation in Idris. |
| 5 | 1 | 5 | 2 years ago | [glfw-idris-st](https://github.com/thalerjonathan/glfw-idris-st)/236 | Bindings for the GLFW library in Idris |
| 5 | 1 | 0 | 6 years ago | [idris-scientific](https://github.com/polasek/idris-scientific)/237 | Exploring the potential use of dependent types in scientific programming. |
| 5 | 0 | 0 | 4 years ago | [idris-sodium](https://github.com/BartAdv/idris-sodium)/238 | A simple Idris implementation of Sodium FRP library, following TypeScript port. WIP |
| 5 | 0 | 1 | 2 years ago | [idris-canvas](https://github.com/trillioneyes/idris-canvas)/239 | Idris bindings to and abstractions over the JavaScript Canvas API |
| 5 | 1 | 0 | 3 years ago | [idris-unicode](https://github.com/Heather/idris-unicode)/240 | :let syntax [a] "→" [b] = a -> b :let syntax λ {x} . [body] = \ x => body |
| 5 | 1 | 1 | 4 years ago | [idris-exercises](https://github.com/stevejb71/idris-exercises)/241 | Exercises from the Idris Type Driven Development book |
| 5 | 0 | 0 | 1 year, 6 months ago | [advent-of-code-2019](https://github.com/tdietert/advent-of-code-2019)/242 | Advent of Code 2019 solutions in Idris |
| 5 | 0 | 0 | 3 years ago | [NomicCoin201710](https://github.com/redfish64/NomicCoin201710)/243 | A p2p network written in Idris and designed to be very similar to idris itself |
| 5 | 1 | 1 | 3 years ago | [setoids](https://github.com/danilkolikov/setoids)/244 | Idris proofs for extensional equalities |
| 5 | 0 | 0 | 4 years ago | [idris-tictactoe](https://github.com/LightAndLight/idris-tictactoe)/245 | TicTacToe using dependent types |
| 5 | 0 | 0 | 1 year, 7 months ago | [idris-heyting-algebra](https://github.com/Risto-Stevcev/idris-heyting-algebra)/246 | Interfaces for heyting algebras and verified bounded join and meet semilattices |
| 5 | 0 | 0 | 2 months ago | [ifui](https://github.com/rbarreiro/ifui)/247 | Idris libraries to create user interfaces |
| 5 | 0 | 0 | 1 year, 7 months ago | [idris-sdl2](https://github.com/corazza/idris-sdl2)/248 | SDL2 bindings for my game in Idris |
| 5 | 0 | 0 | 1 year, 11 months ago | [idris-trees](https://github.com/clayrat/idris-trees)/249 | Trees in Idris |
| 5 | 0 | 0 | 7 years ago | [idris-workshop](https://github.com/puffnfresh/idris-workshop)/250 | Small collection of Idris exercises |
| 5 | 0 | 0 | 4 years ago | [type-driven-develop](https://github.com/xnning/type-driven-develop)/251 | Exercise Solution for the book Type Driven Development with Idris |
| 5 | 2 | 0 | 2 years ago | [rolidris](https://github.com/sqdorte/rolidris)/252 | None |
| 5 | 0 | 1 | 3 years ago | [idris-for-scala-devs](https://github.com/cb372/idris-for-scala-devs)/253 | None |
| 5 | 0 | 0 | 3 years ago | [idris-nanoparsec](https://github.com/lambdaxymox/idris-nanoparsec)/254 | A minimal and simple string based parser combinator library written in Idris. |
| 5 | 0 | 0 | 3 years ago | [roguedris](https://github.com/camelpunch/roguedris)/255 | A Roguelike playground in Idris |
| 5 | 0 | 0 | 2 years ago | [DepSec](https://github.com/simongregersen/DepSec)/256 | A library for static information-flow control in Idris |
| 5 | 1 | 0 | 7 years ago | [idris-finite-math](https://github.com/KesterTong/idris-finite-math)/257 | Math related to finite set and vectors, in Idris |
| 5 | 0 | 0 | 5 months ago | [idris2-scientific](https://github.com/jumper149/idris2-scientific)/258 | Numbers in scientific notation |
| 4 | 0 | 0 | 6 years ago | [programming-in-idris](https://github.com/adelbertc/programming-in-idris)/259 | Following Idris tutorial, also playing around. |
| 4 | 0 | 0 | 2 years ago | [sel4-idris-apps](https://github.com/mokshasoft/sel4-idris-apps)/260 | Example of Idris applications running on the seL4 microkernel |
| 4 | 0 | 0 | 1 year, 5 months ago | [idris-depling](https://github.com/CoderPuppy/idris-depling)/261 | None |
| 4 | 7 | 3 | 1 year, 11 months ago | [idris-sdl2](https://github.com/steshaw/idris-sdl2)/262 | SDL2 binding for Idris |
| 4 | 0 | 0 | 3 years ago | [think-bayes-idris](https://github.com/clayrat/think-bayes-idris)/263 | Think Bayes in Idris |
| 4 | 0 | 0 | 2 years ago | [gl-idris-b](https://github.com/thalerjonathan/gl-idris-b)/264 | Low level OpenGL bindings for Idris |
| 4 | 1 | 0 | 2 years ago | [idris-spring-boot-example](https://github.com/mmhelloworld/idris-spring-boot-example)/265 | Idris Spring Boot example |
| 4 | 0 | 0 | 4 years ago | [idris-playground](https://github.com/ndmitchell/idris-playground)/266 | Playing around with Idris |
| 4 | 0 | 0 | 6 years ago | [Broadhead](https://github.com/japesinator/Broadhead)/267 | Arrow-based parser combinators |
| 4 | 1 | 2 | 1 year, 2 months ago | [togl](https://github.com/dckc/togl)/268 | a Theory of Graphs (by Meredith) |
| 4 | 2 | 0 | 6 years ago | [cooper](https://github.com/forestbelton/cooper)/269 | Presburger arithmetic solver in Idris |
| 4 | 0 | 0 | 12 hours ago | [idris-fix-whitespace](https://github.com/stefan-hoeck/idris-fix-whitespace)/270 | Removes trailing whitespace from .idr files and makes sure they end with exactly one newline. |
| 4 | 0 | 0 | 6 years ago | [idris-protocol-examples](https://github.com/jfdm/idris-protocol-examples)/271 | Examples of using the Idris Protocols package for stuff. |
| 4 | 0 | 0 | 1 year, 18 days ago | [idris-selective](https://github.com/clayrat/idris-selective)/272 | Selective functors in Idris |
| 4 | 0 | 0 | 6 months ago | [aoc-2020](https://github.com/lynn/aoc-2020)/273 | Advent of Code 2020 solutions in Idris 2 |
| 4 | 1 | 0 | 2 months ago | [dao-fp-exercises](https://github.com/rokopt/dao-fp-exercises)/274 | Idris answers to exercises from Bartosz Milewski's _The Dao of Functional Programming_ (https://github.com/BartoszMilewski/Publications/tree/master/TheDaoOfFP) |
| 4 | 0 | 0 | 6 years ago | [ParsingWithProofs](https://github.com/avieth/ParsingWithProofs)/275 | Applicative/monadic parsing with dependent types |
| 4 | 1 | 3 | 2 years ago | [idris-multibase](https://github.com/statebox/idris-multibase)/276 | Self-identifying base encodings in Idris |
| 4 | 4 | 0 | 6 years ago | [idris-curses](https://github.com/tixxit/idris-curses)/277 | Idris bindings to ncurses |
| 4 | 0 | 0 | 3 years ago | [idrisCT](https://github.com/mwpb/idrisCT)/278 | Category Theory Definitions in Idris |
| 4 | 2 | 0 | 7 years ago | [sodium-idris](https://github.com/edwinb/sodium-idris)/279 | Idris bindings for libsodium |
| 4 | 0 | 0 | 5 days ago | [olaf-lang](https://github.com/jfdm/olaf-lang)/280 | None |
| 4 | 0 | 0 | 4 years ago | [incremental](https://github.com/wyn/incremental)/281 | synchronous clocked dataflow in Idris - WIP |
| 4 | 1 | 1 | 1 year, 15 days ago | [learn-idris-pub](https://github.com/stepancheg/learn-idris-pub)/282 | Public data for https://learn-idris.net/ |
| 4 | 0 | 0 | 4 years ago | [IdrisPractice](https://github.com/jwvg0425/IdrisPractice)/283 | Idris Practice |
| 4 | 0 | 0 | 3 months ago | [authenticated_data](https://github.com/mattpolzin/authenticated_data)/284 | Playing with authenticated data structures |
| 4 | 0 | 0 | 3 years ago | [idriscanvas](https://github.com/JinWuZhao/idriscanvas)/285 | idris FFI binding for html5 canvas 2d api |
| 4 | 0 | 0 | 4 years ago | [tdd-idris-ex](https://github.com/stephen-smith/tdd-idris-ex)/286 | Exercise Solutions for Type-Driven Development with Idris |
| 4 | 0 | 0 | 1 year, 6 months ago | [asdf](https://github.com/ostera/asdf)/287 | :bug: Random code snippets  |
| 4 | 0 | 0 | 2 years ago | [cordial](https://github.com/border-patrol/cordial)/288 | A proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions. |
| 4 | 0 | 0 | 2 months ago | [gdris](https://github.com/nmeum/gdris)/289 | A toy gopher client written in Idris2 |
| 4 | 0 | 0 | 6 years ago | [idris-cats](https://github.com/zeitraffer/idris-cats)/290 | some category theory in Idris language |
| 4 | 0 | 0 | 5 years ago | [idris-microKanren](https://github.com/tapeinosyne/idris-microKanren)/291 | μKanren in Idris |
| 4 | 0 | 0 | 8 months ago | [refutation](https://github.com/clayrat/refutation)/292 | Refutation and paraconsistent calculi |
| 4 | 0 | 1 | 11 months ago | [idris-NN](https://github.com/LorenzoPerticone/idris-NN)/293 | Neural Networks in idris |
| 3 | 0 | 0 | 5 years ago | [invincy](https://github.com/defanor/invincy)/294 | Invertible and incremental parsing |
| 3 | 2 | 0 | 4 years ago | [glfw-idris](https://github.com/eckart/glfw-idris)/295 | GLFW bindings for Idris |
| 3 | 0 | 0 | 10 months ago | [gis](https://github.com/yurrriq/gis)/296 | An implementation of David Lewin's Generalized Interval Systems |
| 3 | 0 | 1 | 2 months ago | [idris2-hashmap](https://github.com/Z-snails/idris2-hashmap)/297 | Hash-array map tries in Idris2 |
| 3 | 0 | 0 | 4 years ago | [idris-proofs](https://github.com/hzelenka/idris-proofs)/298 | None |
| 3 | 0 | 1 | 4 years ago | [flow](https://github.com/imuli/flow)/299 | musings on programming with directed acyclic graphs. |
| 3 | 1 | 0 | 4 years ago | [advent-of-code-2016](https://github.com/eeue56/advent-of-code-2016)/300 | None |
| 3 | 0 | 0 | a month ago | [Idris2-hashable](https://github.com/Z-snails/Idris2-hashable)/301 | Interface for types that can be hashed. |
| 3 | 0 | 0 | 2 years ago | [idris-sort](https://github.com/stepancheg/idris-sort)/302 | None |
| 3 | 0 | 0 | 5 years ago | [Synthia](https://github.com/Heather/Synthia)/303 | pseudo package manager |
| 3 | 0 | 0 | 5 years ago | [idris-calc](https://github.com/steshaw/idris-calc)/304 | A simple arithmetic calculator written in Idris. |
| 3 | 0 | 0 | 4 years ago | [libra](https://github.com/ostera/libra)/305 | :balance_scale: A Lisp Parser in Idris |
| 3 | 1 | 0 | 2 years ago | [idris-semidirect](https://github.com/clayrat/idris-semidirect)/306 | Semidirect products for Idris |
| 3 | 0 | 0 | 5 years ago | [idris-benchmarks](https://github.com/bgoodspeed/idris-benchmarks)/307 | Benchmark programs for Idris |
| 3 | 0 | 0 | 7 years ago | [logic-idris](https://github.com/domdere/logic-idris)/308 | proposition combinators in [Idris] |
| 3 | 3 | 0 | 5 years ago | [tomladris](https://github.com/eklavya/tomladris)/309 | TOML parser for Idris |
| 3 | 0 | 0 | 2 months ago | [pearly-razors](https://github.com/border-patrol/pearly-razors)/310 | Code that presents a series of well-typed EDSLs complete with mechanical proofs. |
| 3 | 1 | 2 | 7 years ago | [dyn-universe](https://github.com/trillioneyes/dyn-universe)/311 | Fun with "Dynamic" Typing: An Introduction to Universes |
| 3 | 0 | 0 | 5 months ago | [tdd-with-idris2](https://github.com/JonathanLorimer/tdd-with-idris2)/312 | Working through Type Driven Development with Idris, using Idris2 |
| 3 | 0 | 0 | 3 months ago | [Idris2-HoTT](https://github.com/Russoul/Idris2-HoTT)/313 | Learning me some HoTT in Idris 2 |
| 3 | 2 | 0 | 2 years ago | [type-driven-development-with-idris](https://github.com/juanbono/type-driven-development-with-idris)/314 | Ejercicios del libro Type Driven Development with Idris |
| 3 | 0 | 0 | 5 years ago | [TAPL-idris](https://github.com/ezrosent/TAPL-idris)/315 | Examples of some TAPL examples in the idris language |
| 3 | 0 | 0 | 6 years ago | [FLK-Semantics](https://github.com/ezrosent/FLK-Semantics)/316 | Writing out small-step and big-step operational semantics for the FLK language in Idris |
| 3 | 3 | 0 | 5 years ago | [idris-libmicrohttpd](https://github.com/colin-adams/idris-libmicrohttpd)/317 | A binding of the GNU libmicrohttpd library to the Idris C backend |
| 3 | 0 | 0 | 4 years ago | [learning-idris](https://github.com/yurrriq/learning-idris)/318 | Messy/old Idris notes that don't belong elsewhere. |
| 3 | 0 | 0 | 3 years ago | [idris-hanoi](https://github.com/marcosh/idris-hanoi)/319 | a super type safe implementation of the game of the Tower of Hanoi |
| 3 | 0 | 0 | 3 years ago | [idris-power-of-pi](https://github.com/brendanzab/idris-power-of-pi)/320 | Parts of The Power of Pi, implemented in Idris |
| 3 | 1 | 0 | 2 years ago | [justified-type-inference](https://github.com/joonazan/justified-type-inference)/321 | An implementation of Algorithm W in Idris with a complete proof |
| 3 | 1 | 0 | 2 years ago | [tapl](https://github.com/mr-infty/tapl)/322 | Solutions to the exercises in and miscellaneous material for the book "Types and Programming Languages" by Benjamin C. Pierce. |
| 3 | 0 | 0 | 3 years ago | [Smarter-contract-lang](https://github.com/MrChico/Smarter-contract-lang)/323 | None |
| 3 | 0 | 0 | 3 years ago | [idris-printf](https://github.com/quephird/idris-printf)/324 | A type-safe implementation of `printf` inspired by an exercise from Edwin Brady's TDD in Idris book |
| 3 | 0 | 1 | 3 years ago | [idris-functors](https://github.com/Risto-Stevcev/idris-functors)/325 | Bifunctors and functor products, coproducts, and composition |
| 3 | 0 | 0 | 3 years ago | [spsc-idris](https://github.com/sergei-romanenko/spsc-idris)/326 | A Small Positive Supercompiler in Idris |
| 3 | 1 | 0 | 4 years ago | [type-driven-dev](https://github.com/wyn/type-driven-dev)/327 | exercises from Edwin Brady book 'Type Driven Development with Idris' |
| 3 | 1 | 0 | 3 years ago | [idris-dependent-types](https://github.com/gvolpe/idris-dependent-types)/328 | Dependent Types research in the Idris language |
| 3 | 0 | 0 | 3 years ago | [idris-lambda-reflection](https://github.com/LightAndLight/idris-lambda-reflection)/329 | Reflecting simply-typed lambda calculus into Idris |
| 3 | 0 | 0 | 2 years ago | [idris-datadata](https://github.com/clayrat/idris-datadata)/330 | Datatypes of datatypes |
| 3 | 0 | 0 | 3 years ago | [lambdapants](https://github.com/laserpants/lambdapants)/331 | :sparkles: A REPL for the untyped Lambda Calculus. (Work in progress) |
| 3 | 0 | 0 | 1 year, 10 months ago | [sorts](https://github.com/0xd34df00d/sorts)/332 | Provably correct merge sort |
| 3 | 0 | 0 | 1 year, 9 months ago | [Idris_Category_Theory](https://github.com/bgavran/Idris_Category_Theory)/333 | None |
| 3 | 0 | 0 | 1 year, 5 months ago | [IdrisProofs](https://github.com/LaltonDundy/IdrisProofs)/334 | ExampleProofs using Idris’s Elaborator and Pruviloj |
| 3 | 0 | 0 | 3 years ago | [idris-smtlib](https://github.com/clayrat/idris-smtlib)/335 | SMT-LIB text interface for Idris |
| 3 | 0 | 0 | 7 years ago | [idfXt](https://github.com/paulkoerbitz/idfXt)/336 | An Xmonad clone written in Idris |
| 3 | 1 | 0 | 3 years ago | [IdrisExperiments](https://github.com/QuentinDuval/IdrisExperiments)/337 | None |
| 3 | 0 | 0 | 2 years ago | [libsel4-idris-ffi](https://github.com/mokshasoft/libsel4-idris-ffi)/338 | An Idris FFI to the libsel4 library |
| 3 | 0 | 0 | 5 years ago | [lambductive](https://github.com/shlevy/lambductive)/339 | A lambda calculus with tarski universes, pi types, and self-referential expressions |
| 3 | 1 | 1 | a month ago | [katla](https://github.com/ohad/katla)/340 | None |
| 3 | 0 | 0 | 5 years ago | [SimpleTypes](https://github.com/wspk/SimpleTypes)/341 | Implementation and verification of the Simply Typed Lambda Calculus using Idris |
| 3 | 0 | 0 | 6 years ago | [ConorLearnsIdris](https://github.com/pigworker/ConorLearnsIdris)/342 | being a scratch space for my teething troubles and tiny triumphs |
| 3 | 0 | 0 | 6 years ago | [simulation](https://github.com/gavlegoat/simulation)/343 | An electronic circuit simulator using Idris |
| 3 | 0 | 0 | 3 years ago | [composition](https://github.com/vmchale/composition)/344 | Composition extras for Idris |
| 3 | 0 | 0 | 3 years ago | [Mapping.idr](https://github.com/zaoqi/Mapping.idr)/345 | None |
| 3 | 5 | 0 | 22 days ago | [SNU_2D_ProgrammingTools_IDE_Idris](https://github.com/seanpm2001/SNU_2D_ProgrammingTools_IDE_Idris)/346 | The Idris Programming language IDE submodule for SNU Programming Tools (2D Mode)  |
| 2 | 0 | 0 | 7 years ago | [Meetup-Materials](https://github.com/HaskellDC/Meetup-Materials)/347 | None |
| 2 | 0 | 0 | 4 years ago | [DOS2016_IdrisWorkshop](https://github.com/CarstenKoenig/DOS2016_IdrisWorkshop)/348 | Materialien und Infos für meinen Workshop auf dem Developer Open Space 2016 in Leipzig |
| 2 | 0 | 0 | 4 years ago | [idris-miniml](https://github.com/steshaw/idris-miniml)/349 | Compiler for MiniML in Idris |
| 2 | 1 | 0 | 2 years ago | [depennd](https://github.com/rossng/depennd)/350 | A very hacky (and incomplete - no backprop!) Neural Network implementation with dependent types |
| 2 | 0 | 4 | 4 years ago | [advent-of-idris](https://github.com/yurrriq/advent-of-idris)/351 | My Idris (and Haskell) solutions to the 2016 Advent of Code. |
| 2 | 0 | 0 | 2 years ago | [Numdris](https://github.com/njjiang/Numdris)/352 | A linear algebra library in Idris |
| 2 | 0 | 0 | 1 year, 8 months ago | [IdrisTest](https://github.com/marcesquerra/IdrisTest)/353 | Testing library for Idris |
| 2 | 0 | 0 | 6 years ago | [idris-xml-simple](https://github.com/LeifW/idris-xml-simple)/354 | Simple XML ADT for Idris |
| 2 | 0 | 0 | 7 years ago | [idris-directory](https://github.com/trillioneyes/idris-directory)/355 | None |
| 2 | 1 | 0 | 4 years ago | [idris-koans](https://github.com/simonewebdesign/idris-koans)/356 | The path to enlightenment |
| 2 | 2 | 0 | 2 years ago | [YCombinator](https://github.com/jutaro/YCombinator)/357 | Excercises from riddle book "To mock a Mockingbird" |
| 2 | 0 | 0 | 1 year, 7 months ago | [idris-jvm-auto-ffi-sample](https://github.com/mmhelloworld/idris-jvm-auto-ffi-sample)/358 | Idris JVM automated FFI example |
| 2 | 0 | 0 | 1 year, 5 months ago | [bare-metal-idris-drivers](https://github.com/mokshasoft/bare-metal-idris-drivers)/359 | Drivers written in Idris for bare-metal apps |
| 2 | 0 | 1 | 1 year, 1 month ago | [dasheri](https://github.com/jeetu7/dasheri)/360 | Matrix type data store for Idris2 |
| 2 | 0 | 0 | 7 months ago | [advanced-software-analysis](https://github.com/JnxF/advanced-software-analysis)/361 | :robot: Advanced Software Analysis |
| 2 | 0 | 0 | a month ago | [idris2-complete](https://github.com/stefan-hoeck/idris2-complete)/362 | Tab completion for Idris2 |
| 2 | 0 | 0 | 5 years ago | [idris-misc](https://github.com/bgoodspeed/idris-misc)/363 | Miscellaneous Idris functions/types/etc  |
| 2 | 0 | 0 | 3 years ago | [idris-samples](https://github.com/sergei-romanenko/idris-samples)/364 | A collection of samples in Idris |
| 2 | 0 | 3 | 1 year, 11 months ago | [ImpCompiler](https://github.com/RonaldCamp/ImpCompiler)/365 | None |
| 2 | 2 | 0 | 5 years ago | [idris-libwebsockets](https://github.com/colin-adams/idris-libwebsockets)/366 | An Idris wrapper around libwebsockets |
| 2 | 1 | 0 | 3 years ago | [idris-comonad](https://github.com/Risto-Stevcev/idris-comonad)/367 | An implementation of comonads in idris |
| 2 | 0 | 0 | 2 years ago | [regalloc](https://github.com/elpinal/regalloc)/368 | Training in register allocation |
| 2 | 0 | 0 | 3 days ago | [idris-gimel](https://github.com/DoctorRyner/idris-gimel)/369 | None |
| 2 | 0 | 0 | 7 years ago | [validation-idris](https://github.com/domdere/validation-idris)/370 | Port of the Validation Library to Idris |
| 2 | 0 | 0 | 11 months ago | [type-preserving-crossover](https://github.com/donovancrichton/type-preserving-crossover)/371 | A verified, type-preserving, crossover method for well-typed higher order abstract syntax trees |
| 2 | 0 | 0 | 5 months ago | [idris2-json](https://github.com/jumper149/idris2-json)/372 | Idris JSON library |
| 2 | 0 | 0 | 3 months ago | [ia](https://github.com/brainrape/ia)/373 | Idris Async IO |
| 2 | 0 | 0 | 5 months ago | [idris2-subsets](https://github.com/stefan-hoeck/idris2-subsets)/374 | A library for runtime-checked refinement types |
| 2 | 2 | 0 | 7 years ago | [GameTheory-Idris](https://github.com/walkie/GameTheory-Idris)/375 | A behavioral game theory library in Idris. |
| 2 | 0 | 0 | 7 years ago | [idris-talk](https://github.com/markhibberd/idris-talk)/376 | None |
| 2 | 0 | 1 | 3 years ago | [tydd-with-idris-notes](https://github.com/missingfaktor/tydd-with-idris-notes)/377 | Notes I jot down as I work through the book "Type-Driven Development with Idris" |
| 2 | 0 | 0 | 3 years ago | [idris-school](https://github.com/NashFP/idris-school)/378 | Materials for NashFP's monthly learning Idris sessions |
| 2 | 1 | 0 | 2 years ago | [idris-type-driven-development-exercises](https://github.com/robkorn/idris-type-driven-development-exercises)/379 | Exercises From Type Driven Development With Idris |
| 2 | 0 | 0 | 3 years ago | [preger](https://github.com/clayrat/preger)/380 | Presburger solver |
| 2 | 0 | 0 | 1 year, 9 months ago | [jacekFFI](https://github.com/bigos/jacekFFI)/381 | None |
| 2 | 0 | 0 | 6 years ago | [vm-playground](https://github.com/danielwaterworth/vm-playground)/382 | Fun making virtual machines, probably won't come to much. |
| 2 | 0 | 0 | 7 years ago | [idris-tutorial](https://github.com/eckart/idris-tutorial)/383 | A tutorial to explain Idris to myself |
| 2 | 1 | 1 | 2 years ago | [comonad](https://github.com/vmchale/comonad)/384 | Comonads for Idris |
| 2 | 0 | 0 | 7 months ago | [idris2-server](https://github.com/ska80/idris2-server)/385 | A dependently typed server framework for Idris |
| 2 | 0 | 0 | 6 months ago | [aoc-2020-idris](https://github.com/xWafl/aoc-2020-idris)/386 | Advent of Code 2020 |
| 2 | 1 | 3 | 5 years ago | [idris-split](https://github.com/relrod/idris-split)/387 | An almost-direct port of Brent Yorgey's "split" package to Idris. |
| 2 | 0 | 0 | 3 years ago | [idris-raytracer](https://github.com/pa-ba/idris-raytracer)/388 | simple ray tracer implemented in Idris |
| 2 | 0 | 0 | a month ago | [eff](https://github.com/gh-archived/eff)/389 | (W.I.P.) Resource-dependent algebraic effects library  in Idris 2. |
| 2 | 0 | 1 | 26 days ago | [idris-free](https://github.com/gallais/idris-free)/390 | Various Free-X experiments |
| 2 | 0 | 0 | 5 days ago | [veribase-idr2](https://github.com/LibreCybernetics/veribase-idr2)/391 | Veribase Idris2 [MIRROR] |
| 2 | 0 | 0 | 6 years ago | [idris-rosetta](https://github.com/havleoto/idris-rosetta)/392 | Learning Idris through tasks from Rosseta Code |
| 2 | 0 | 0 | 4 years ago | [idris-loader](https://github.com/mmn80/idris-loader)/393 | Dynamic loading of Idris modules |
| 2 | 0 | 0 | 1 year, 5 months ago | [bare-metal-idris-apps](https://github.com/mokshasoft/bare-metal-idris-apps)/394 | Idris apps that run on bare-metal |
| 2 | 0 | 0 | 6 years ago | [Idris-DOM](https://github.com/jaredloomis/Idris-DOM)/395 | Idris wrapper over some of the JavaScript DOM, with a FRP module included. |
| 2 | 0 | 0 | 3 years ago | [idris-hlist](https://github.com/gdefacci/idris-hlist)/396 | None |
| 2 | 0 | 0 | 4 years ago | [IdrisTrainReservationKata](https://github.com/QuentinDuval/IdrisTrainReservationKata)/397 | None |
| 2 | 0 | 0 | 1 year, 2 months ago | [resources](https://github.com/border-patrol/resources)/398 | A framework for Resource Dependent EDSLs in a Dependently Typed Language. |
| 2 | 1 | 0 | 1 year, 2 months ago | [Dynamical](https://github.com/DavidJaz/Dynamical)/399 | Open Monadic Dependent Dynamical Systems... in Idris |
| 2 | 0 | 0 | 1 year, 6 months ago | [aoc-2019](https://github.com/fabianhjr/aoc-2019)/400 | Advent of Code 2019 in Idris |
| 2 | 0 | 0 | 6 months ago | [advent-of-code](https://github.com/andorp/advent-of-code)/401 | None |
| 2 | 0 | 0 | a month ago | [pg-idris](https://github.com/mattpolzin/pg-idris)/402 | Beginnings of a Postgres client for Idris 2 |
| 2 | 0 | 0 | 5 years ago | [idris-grl](https://github.com/jfdm/idris-grl)/403 | An implementation of the Goal Requirements Language in Idris. |
| 2 | 2 | 1 | 5 years ago | [ConcProc](https://github.com/edwinb/ConcProc)/404 | Concurrent process DSL |
| 2 | 0 | 0 | 5 years ago | [idris-strings](https://github.com/bgoodspeed/idris-strings)/405 | String (word) representations and proof for Idris |
| 2 | 0 | 1 | 4 years ago | [idris-dom](https://github.com/pierrebeaucamp/idris-dom)/406 | An Idris library to interact with the DOM |
| 2 | 0 | 0 | 3 years ago | [idris-norm-by-traversals](https://github.com/sergei-romanenko/idris-norm-by-traversals)/407 | Traversal-based normalization for ULC |
| 2 | 0 | 0 | 2 years ago | [idris-book](https://github.com/pascalpoizat/idris-book)/408 | examples and exercises in "Type-Driven Development with Idris" |
| 2 | 0 | 0 | 1 year, 2 months ago | [flexidisc](https://github.com/LIST-LUXEMBOURG/flexidisc)/409 | Typesafe extensible records (and more) for Idris. |
| 2 | 0 | 0 | 9 months ago | [idris-music](https://github.com/witt3rd/idris-music)/410 | Learning Idris through recreational coding |
| 2 | 0 | 0 | 4 years ago | [idris-regexp](https://github.com/taktoa/idris-regexp)/411 | Regular expressions in Idris |
| 2 | 1 | 0 | 7 years ago | [idris-sdl2](https://github.com/deweyvm/idris-sdl2)/412 | None |
| 2 | 0 | 0 | 5 years ago | [monoid-prover](https://github.com/rodrigogribeiro/monoid-prover)/413 | A reflective tactic for proving monoid equalities in Idris |
| 2 | 0 | 0 | 6 years ago | [Eff-dev](https://github.com/edwinb/Eff-dev)/414 | Development version of effects library for Idris |
| 2 | 1 | 1 | 5 years ago | [STLC](https://github.com/jcsmnt0/STLC)/415 | Simply-typed lambda calculus in Idris |
| 2 | 0 | 0 | 1 year, 11 months ago | [Idris-Repl](https://github.com/zenntenn/Idris-Repl)/416 | A self hosted Repl for Idris (Still *very* early stages) |
| 2 | 1 | 0 | 3 years ago | [bfjit-idr](https://github.com/edmundsmith/bfjit-idr)/417 | Brainfuck JIT/Compiler made with Idris |
| 2 | 0 | 0 | 3 years ago | [archer](https://github.com/tuura/archer)/418 | An experimental embedded domain specific language for describing instruction set architectures semantics. |
| 2 | 2 | 0 | 3 years ago | [Idris-Number-Theory](https://github.com/anotherArka/Idris-Number-Theory)/419 | Elementary number theory written in Idris. |
| 2 | 0 | 0 | 2 years ago | [verified-tensor-operations](https://github.com/emilyaherbert/verified-tensor-operations)/420 | Attempt at creating a tensor type in Idris with dimension-safe operations. |
| 2 | 0 | 2 | 5 years ago | [BonjourToUnbound](https://github.com/jeremy-w/BonjourToUnbound)/421 | Pretend MyHomeNAS.local is SomeURL.com by rewriting records from a Bonjour query as Unbound local_data entries |
| 2 | 0 | 1 | 4 years ago | [rational-setoid](https://github.com/zerogerc/rational-setoid)/422 | setoid for rational numbers in Idris |
| 2 | 0 | 0 | 1 year, 5 months ago | [MATH302](https://github.com/tkaden4/MATH302)/423 | WWU MATH 302 Proofs in Idris |
| 2 | 0 | 0 | 1 year, 6 months ago | [adventofcode2019](https://github.com/Carreau/adventofcode2019)/424 | None |
| 2 | 0 | 0 | 2 months ago | [learn-idris](https://github.com/melwyn95/learn-idris)/425 | Notes & Exercise solutions of TDD  with Idris |
| 2 | 2 | 0 | 2 years ago | [Bikini](https://github.com/Heather/Bikini)/426 | Bad experiment | C++ Syntax Wrapper |
| 2 | 0 | 0 | 2 years ago | [idris-alga](https://github.com/yurrriq/idris-alga)/427 | The theory of algebraic graphs formalised in Idris |
| 2 | 0 | 0 | 2 years ago | [idris-groups](https://github.com/stop-cran/idris-groups)/428 | Groups as T-algebras and group presentations. |
| 2 | 0 | 0 | 5 years ago | [idris-game-of-life](https://github.com/bamboo/idris-game-of-life)/429 | An implementation of Conway's Game Of Life in Idris |
| 2 | 0 | 0 | 5 years ago | [idris-optics](https://github.com/justjoheinz/idris-optics)/430 | None |
| 2 | 0 | 0 | 7 years ago | [newmod](https://github.com/esmooov/newmod)/431 | None |
| 2 | 0 | 0 | 11 months ago | [idris2-perf](https://github.com/ziman/idris2-perf)/432 | Various benchmarks |
| 2 | 0 | 0 | 11 days ago | [ncurses-idris](https://github.com/mattpolzin/ncurses-idris)/433 | A hobby implementation of an ncurses binding for Idris 2 |
| 2 | 0 | 0 | 10 days ago | [idris-react-example](https://github.com/DoctorRyner/idris-react-example)/434 | None |
| 2 | 0 | 0 | 1 year, 5 months ago | [Idris2-pkg-outline](https://github.com/edwinb/Idris2-pkg-outline)/435 | Outline of an Idris2 package which uses C glue |
| 1 | 0 | 0 | 6 years ago | [idris-linear-algebra](https://github.com/jeffersoncarpenter/idris-linear-algebra)/436 | a Linear Algebra library for Idris |
| 1 | 0 | 1 | 4 years ago | [idris-catenable-lists](https://github.com/Risto-Stevcev/idris-catenable-lists)/437 | A port of the purescript catenable-lists library in Idris |
| 1 | 0 | 0 | 3 years ago | [seo-router](https://github.com/janschultecom/seo-router)/438 | None |
| 1 | 0 | 0 | 3 years ago | [sv](https://github.com/chameco/sv)/439 | Software Verification - Spring 2018 |
| 1 | 0 | 0 | 4 years ago | [idris-sandbox](https://github.com/esmolanka/idris-sandbox)/440 | None |
| 1 | 0 | 0 | 2 years ago | [advent-of-shame-2018](https://github.com/dmalikov/advent-of-shame-2018)/441 | I'll drop tomorrow | s/::/:/g et voila! |
| 1 | 0 | 0 | 1 year, 6 months ago | [unification](https://github.com/clayrat/unification)/442 | unification algorithms in Idris |
| 1 | 0 | 0 | 10 months ago | [idris2-curl](https://github.com/wchresta/idris2-curl)/443 | Curl bindings for Idris 2 |
| 1 | 0 | 3 | 3 months ago | [mysql-idris2](https://github.com/thomasdziedzic/mysql-idris2)/444 | Mysql library for Idris2. |
| 1 | 1 | 0 | 22 days ago | [DemoIdris](https://github.com/haetze/DemoIdris)/445 | None |
| 1 | 0 | 0 | 2 years ago | [namespace2xml-idris](https://github.com/stop-cran/namespace2xml-idris)/446 | None |
| 1 | 0 | 0 | 3 years ago | [Idris-Conway](https://github.com/RossMeikleham/Idris-Conway)/447 | Conway's Game Of Life Implementation in Idris |
| 1 | 0 | 0 | 5 years ago | [idris-misc](https://github.com/portnov/idris-misc)/448 | None |
| 1 | 0 | 0 | 4 years ago | [Lambda-Calculus](https://github.com/Stoicheion/Lambda-Calculus)/449 | None |
| 1 | 0 | 0 | 3 years ago | [compiler-construction](https://github.com/SalWolffs/compiler-construction)/450 | None |
| 1 | 0 | 0 | 2 years ago | [learning-idris](https://github.com/gauntwa/learning-idris)/451 | My idris learning exercises |
| 1 | 0 | 0 | 4 years ago | [idris-absint](https://github.com/taktoa/idris-absint)/452 | Abstract interpretation in Idris |
| 1 | 0 | 0 | 1 year, 8 months ago | [idris-functors](https://github.com/clayrat/idris-functors)/453 | Functors |
| 1 | 0 | 1 | 1 year, 9 months ago | [lidrisp](https://github.com/ebenpack/lidrisp)/454 | A scheme-like written in idris |
| 1 | 0 | 0 | 2 years ago | [idris-algebra](https://github.com/buonuomo/idris-algebra)/455 | Proving algebraic properties using Idris |
| 1 | 0 | 0 | 2 years ago | [idris-rationals](https://github.com/marcosh/idris-rationals)/456 | rational numbers in Idris |
| 1 | 0 | 0 | 1 year, 3 months ago | [Dai](https://github.com/zenntenn/Dai)/457 | An Idris automation tool designed to assist with behavior-driven development, based on Cucumber/Gherkin to support type-driven development |
| 1 | 1 | 0 | 1 year, 8 months ago | [idris-experiments](https://github.com/andrevidela/idris-experiments)/458 | None |
| 1 | 0 | 0 | 1 year, 6 months ago | [idrisHW](https://github.com/Domonion/idrisHW)/459 | None |
| 1 | 0 | 0 | 5 years ago | [sif-lang](https://github.com/jfdm/sif-lang)/460 | A Requirements Oriented DSL for design pattern specification. |
| 1 | 0 | 0 | 7 years ago | [idris-jsglmatrix](https://github.com/mankyKitty/idris-jsglmatrix)/461 | FFI Wrapper for GLMatrix JS Lib in Idris |
| 1 | 0 | 1 | 5 years ago | [void.idr](https://github.com/PolyglotSymposium/void.idr)/462 | Experimental Vim-like editor in Idris |
| 1 | 0 | 3 | 1 year, 8 months ago | [clippings](https://github.com/yurrriq/clippings)/463 | Parser for Kindle clippings. |
| 1 | 0 | 0 | 4 years ago | [idris-ioref-c](https://github.com/BartAdv/idris-ioref-c)/464 | Basic IORefs for Idris (with C backend) |
| 1 | 0 | 0 | 3 years ago | [tdd_with_idris](https://github.com/kevinmeredith/tdd_with_idris)/465 | Working on exercises and lectures of TDD with Idris (manning book) |
| 1 | 0 | 0 | 3 years ago | [idris](https://github.com/Nikolaj-K/idris)/466 | Code files from the youtube series on Idris |
| 1 | 0 | 0 | 3 years ago | [tdd-with-idris](https://github.com/quephird/tdd-with-idris)/467 | Solutions to exercises for the brilliant book |
| 1 | 0 | 0 | 3 years ago | [NYC-Idris](https://github.com/maitria/NYC-Idris)/468 | Notes and random things from the NYC Idris meetup |
| 1 | 0 | 0 | 3 years ago | [chip8i](https://github.com/cantsin/chip8i)/469 | Chip8 emulator written in Idris |
| 1 | 0 | 0 | 2 months ago | [cosmos-idris](https://github.com/soareschen/cosmos-idris)/470 | Tendermint, IBC, and Cosmos Blockchain Specification in Idris |
| 1 | 0 | 0 | 2 years ago | [idris-elba-example](https://github.com/steshaw/idris-elba-example)/471 | None |
| 1 | 0 | 0 | 2 years ago | [equis](https://github.com/lambdacasserole/equis)/472 | A library for solving systems of linear equations, using Idris. |
| 1 | 1 | 0 | 1 year, 6 months ago | [idris-graph-toy](https://github.com/xiphiness/idris-graph-toy)/473 | None |
| 1 | 0 | 0 | 1 year, 1 month ago | [idris-dhcli](https://github.com/gallais/idris-dhcli)/474 | Declarative Hierarchical Command Line Interfaces |
| 1 | 0 | 27 | 22 hours ago | [spidr](https://github.com/joelberkeley/spidr)/475 | Marrying research in probabilistic modelling, language theory and hardware accelerators. |
| 1 | 0 | 0 | 6 years ago | [eckner](https://github.com/lmarburger/eckner)/476 | Implementing timeseries analysis functions from the Eckner paper. |
| 1 | 0 | 0 | 6 years ago | [idris-graph](https://github.com/rizo/idris-graph)/477 | Minimal graph model implementation in Idris. |
| 1 | 0 | 0 | 5 years ago | [crypto-idris](https://github.com/juxtin/crypto-idris)/478 | None |
| 1 | 0 | 0 | 5 years ago | [SILL-Idris](https://github.com/ISANobody/SILL-Idris)/479 | An Implementaiton of substructrual session types in Idris |
| 1 | 0 | 0 | 6 years ago | [complex](https://github.com/japesinator/complex)/480 | Messing around with complex numbers in idris |
| 1 | 0 | 0 | 3 years ago | [simple-bmp](https://github.com/spearman/simple-bmp)/481 | Create and write 32-bit RGBA BMP files |
| 1 | 0 | 0 | 3 years ago | [idris-vecspace](https://github.com/clayrat/idris-vecspace)/482 | Abstract vector spaces in Idris |
| 1 | 1 | 0 | 3 years ago | [baseline-idris](https://github.com/laserpants/baseline-idris)/483 | Minimal readline-like API for Idris. |
| 1 | 0 | 0 | 3 years ago | [DependentLambda](https://github.com/xtreme-james-cooper/DependentLambda)/484 | Rather simple enriched lambda calculus, done in Idris |
| 1 | 0 | 0 | 2 years ago | [FerryJS](https://github.com/leon-vv/FerryJS)/485 | A ferry between Idris land and JavaScript land: convert values easily |
| 1 | 0 | 0 | 2 years ago | [learning-tparsec](https://github.com/andreykl/learning-tparsec)/486 | just experiments with gallais paper  |
| 1 | 0 | 0 | 4 months ago | [idris-js-example](https://github.com/DoctorRyner/idris-js-example)/487 | None |
| 1 | 0 | 0 | 4 months ago | [idris-adds](https://github.com/mattpolzin/idris-adds)/488 | Random Idris 2 stuff that might be generally useful to me in the future. |
| 1 | 0 | 6 | 4 months ago | [mute-text-to-speech](https://github.com/guardians-of-life/mute-text-to-speech)/489 | Mutes text-to-speech when someone is talking over Discord |
| 1 | 0 | 0 | 3 months ago | [Idris-Applied-Category-Theory](https://github.com/lemastero/Idris-Applied-Category-Theory)/490 | Implementation of concepts from Applied Category Theory |
| 1 | 0 | 0 | 6 years ago | [tic-tac-idris](https://github.com/davidfstr/tic-tac-idris)/491 | Tic-tac-toe game written in Idris. |
| 1 | 0 | 0 | 5 years ago | [idris-uml](https://github.com/jfdm/idris-uml)/492 | A simple DSL for UML modelling together with an API for programmable access. |
| 1 | 0 | 0 | 6 years ago | [andromeda-idris](https://github.com/jaredloomis/andromeda-idris)/493 | A GLSL representation and eDSL in Idris |
| 1 | 0 | 0 | 3 years ago | [idris-talk](https://github.com/k-bx/idris-talk)/494 | None |
| 1 | 0 | 0 | 2 years ago | [idr-pure-prolog](https://github.com/Sintrastes/idr-pure-prolog)/495 | Embeded Prolog DSL written in Idris. Based on github.com/kfl/pure-prolog. |
| 1 | 0 | 0 | 1 year, 10 months ago | [tulis](https://github.com/PeterHajdu/tulis)/496 | A small game to teach programming |
| 1 | 0 | 0 | 5 months ago | [AoC2020](https://github.com/jumper149/AoC2020)/497 | My solutions to the Advent of Code 2020 exercises |
| 1 | 0 | 0 | 10 months ago | [dmmf](https://github.com/andorp/dmmf)/498 | Examples from the 'Domain Modeling made Functional' book. |
| 1 | 0 | 1 | 4 months ago | [idris2-managed](https://github.com/MarcelineVQ/idris2-managed)/499 | Automatic resource management for a common use-pattern. |
| 1 | 0 | 0 | 2 months ago | [SortingAlgs](https://github.com/cmzou/SortingAlgs)/500 | Final CS390 Project using the Idris language to implement and prove sorting algorithms |
| 1 | 0 | 0 | 14 hours ago | [idris2-pretty-show](https://github.com/stefan-hoeck/idris2-pretty-show)/501 | None |
| 1 | 0 | 0 | 6 years ago | [marko](https://github.com/trillioneyes/marko)/502 | Dissociated Press in Idris |
| 1 | 0 | 0 | 5 years ago | [idris-graph](https://github.com/yacinehmito/idris-graph)/503 | A library to create, manipulate and draw graphs |
| 1 | 0 | 0 | 4 years ago | [idris-webgl](https://github.com/pierrebeaucamp/idris-webgl)/504 | An Idris library to interact with WebGL |
| 1 | 0 | 0 | 3 years ago | [idris-todaybot](https://github.com/benclifford/idris-todaybot)/505 | An Idris implementation of lsc-todaybot - a bot which moves the [TODAY] flair around on reddit.com/r/LondonSocialClub |
| 1 | 1 | 0 | 4 years ago | [pl-sem-jr-2017-summer](https://github.com/ulysses4ever/pl-sem-jr-2017-summer)/506 | None |
| 1 | 0 | 0 | 3 years ago | [marshal](https://github.com/clayrat/marshal)/507 | serialization for Idris |
| 1 | 0 | 0 | 3 years ago | [idris-typescript](https://github.com/goodmind/idris-typescript)/508 | None |
| 1 | 0 | 0 | 3 years ago | [idris-hitchhiker-tree](https://github.com/yurrriq/idris-hitchhiker-tree)/509 | An Idris implementation of hitchhiker trees. |
| 1 | 0 | 0 | 2 years ago | [Record](https://github.com/leon-vv/Record)/510 | Idris package describing records directly using sum types |
| 1 | 0 | 1 | 3 years ago | [idris-algebra](https://github.com/jdublu10/idris-algebra)/511 | An attempt at proving algebra theorems in idris |
| 1 | 0 | 0 | 2 years ago | [semver](https://github.com/elba/semver)/512 | A semantic versioning library in Idris |
| 1 | 0 | 0 | 1 year, 11 months ago | [gspider](https://github.com/sr-lab/gspider)/513 | Guess success probability slider, for plotting the evolution of password guessing attacks. |
| 1 | 1 | 0 | 2 months ago | [idris_dsp_circuits](https://github.com/cramsay/idris_dsp_circuits)/514 | None |
| 1 | 0 | 0 | 10 months ago | [idris-ct-studies](https://github.com/andorp/idris-ct-studies)/515 | Basic category theory studies in Idris2 |
| 1 | 6 | 0 | Unknown | [inigo](https://github.com/bbarker/inigo)/516 | Inigo: A Package Manager for Idris2 |
| 1 | 0 | 0 | Unknown | [idris-playground](https://github.com/buzden/idris-playground)/517 | Personal playground for Idris stuff |
| 1 | 0 | 0 | Unknown | [DependentLinearProgramming](https://github.com/dshieble/DependentLinearProgramming)/518 | None |
| 1 | 0 | 0 | Unknown | [idris-even](https://github.com/andrevidela/idris-even)/519 | Small library to deal with even numbers and vectors of even length |
| 1 | 0 | 0 | Unknown | [tdd-with-idris](https://github.com/yurrriq/tdd-with-idris)/520 | :book: Working through Type-Driven Development with Idris |
| 1 | 0 | 0 | Unknown | [9p2000](https://github.com/markuspf/9p2000)/521 | Plan9 protocol implementation in Idris using @edwinb's Protocols |
| 1 | 0 | 0 | Unknown | [type-driven-development](https://github.com/tekerson/type-driven-development)/522 | Working through the exercises from @edwinb's "Type Driven Development with Idris" (https://www.manning.com/books/type-driven-development-with-idris) |
| 1 | 0 | 0 | Unknown | [iditty](https://github.com/nicklecompte/iditty)/523 | terminal control / emulation / ui in Idris |
| 1 | 0 | 0 | Unknown | [idris-js](https://github.com/jheiling/idris-js)/524 | Js library for Idris |
| 1 | 0 | 0 | Unknown | [oplss-note](https://github.com/xieyuheng/oplss-note)/525 | oplss note |
| 1 | 0 | 0 | Unknown | [code-for-lectures](https://github.com/buzden/code-for-lectures)/526 | Code that @buzden used for lectures and talks on functional programming |
| 1 | 0 | 0 | Unknown | [Resources](https://github.com/edwinb/Resources)/527 | None |
| 1 | 0 | 3 | Unknown | [fun](https://github.com/alexFrankfurt/fun)/528 | Small idris examples |
| 1 | 1 | 0 | Unknown | [type-driven-development-with-idris](https://github.com/ruippeixotog/type-driven-development-with-idris)/529 | My solutions to "Type-Driven Development with Idris" exercises |
| 1 | 0 | 0 | Unknown | [iterm](https://github.com/PeterHajdu/iterm)/530 | Simple tools to build interactive terminal applications. |
| 1 | 0 | 0 | Unknown | [idris](https://github.com/emres/idris)/531 | Repository for Idris programming self-study |
| 1 | 0 | 0 | Unknown | [Http](https://github.com/leon-vv/Http)/532 | Http module for Idris (small wrapper around Node.js) |
| 1 | 0 | 0 | Unknown | [queries.idr](https://github.com/Kazark/queries.idr)/533 | An investigation into DSLs with free monads and queries etc, using Idris |
| 1 | 0 | 0 | Unknown | [path](https://github.com/elba/path)/534 | Well-typed paths in Idris |
| 1 | 0 | 0 | Unknown | [tdd-with-idris](https://github.com/dzhus/tdd-with-idris)/535 | Idris book excercises |
| 1 | 0 | 0 | Unknown | [idris-websocket](https://github.com/concert/idris-websocket)/536 | A toy websocket library for Idris |
| 1 | 0 | 0 | Unknown | [notes-on-tdd](https://github.com/ChristianoBraga/notes-on-tdd)/537 | Notes on type-driven development in Idris |
| 1 | 0 | 0 | Unknown | [idris-order](https://github.com/clayrat/idris-order)/538 | Order/domain theory |
| 1 | 1 | 0 | Unknown | [brainfeck](https://github.com/jhmcstanton/brainfeck)/539 | Brainfuck interpreter written in Idris |
| 1 | 0 | 0 | Unknown | [untyped-lc](https://github.com/eayus/untyped-lc)/540 | Simple untyped lambda calculus interpreter in Idris |
| 1 | 1 | 0 | Unknown | [idris-sqlite3](https://github.com/MarcelineVQ/idris-sqlite3)/541 | bindings to sqlite in idris2 |
| 1 | 0 | 0 | Unknown | [PLFA-idris](https://github.com/andrevidela/PLFA-idris)/542 | PLFA exercises in IDris |
| 1 | 0 | 0 | Unknown | [Idris-different](https://github.com/ZhekehZ/Idris-different)/543 | None |
| 1 | 0 | 0 | Unknown | [Toml](https://github.com/Chiyoku/Toml)/544 | Toml parser for Idris1 Language. |
| 1 | 0 | 0 | Unknown | [tester-idr](https://github.com/tiatomee/tester-idr)/545 | Small testing framework for Idris 2 |
| 1 | 0 | 0 | Unknown | [hott](https://github.com/silky/hott)/546 | HoTT in Idris |
| 1 | 0 | 0 | Unknown | [BoehmBerarducci](https://github.com/sammthomson/BoehmBerarducci)/547 | playing around with Boehm-Berarducci encodings in Idris |
| 1 | 0 | 0 | Unknown | [tdd-idris](https://github.com/joaomilho/tdd-idris)/548 | just exercises |
| 1 | 0 | 0 | Unknown | [lc.idr](https://github.com/Kazark/lc.idr)/549 | Attempt at implementing lambda calculus in Idris |
| 1 | 0 | 0 | Unknown | [idris-algebra](https://github.com/anotherArka/idris-algebra)/550 | Formalization of algebra in Idris |
| 1 | 0 | 0 | Unknown | [idris-money](https://github.com/pawelsawicz/idris-money)/551 | Dependently typed money |
| 1 | 0 | 0 | Unknown | [idris-collections](https://github.com/polendri/idris-collections)/552 | Verified data structures in Idris 2 |
| 1 | 0 | 0 | Unknown | [idris-type-driven-development](https://github.com/witt3rd/idris-type-driven-development)/553 | Worked examples from "Type-Driven Development with Idris" using Idris2 |
| 1 | 1 | 1 | Unknown | [idris2-sdl](https://github.com/ShinKage/idris2-sdl)/554 | Experimental SDL2 bindings for Idris2 |
| 1 | 0 | 0 | Unknown | [lambdadome](https://github.com/jfdm/lambdadome)/555 | None |
| 1 | 0 | 0 | Unknown | [Daudbpp2021](https://github.com/Daudbpp2021/Daudbpp2021)/556 | Config files for my GitHub profile. |
| 1 | 1 | 0 | Unknown | [Idris](https://github.com/GCPBigData/Idris)/557 | Meus Estudos sobre essa linguagem Fantastica [->] Idris |
| 1 | 0 | 0 | Unknown | [NewEden](https://github.com/identicalsnowflake/NewEden)/558 | Polymorphic, axiom-based implementation of common types |
| 1 | 0 | 0 | Unknown | [idris-sandbox](https://github.com/srdqty/idris-sandbox)/559 | Experiments with the Idris programming language |
| 1 | 0 | 0 | Unknown | [andrewbrucenet](https://github.com/camelpunch/andrewbrucenet)/560 | A bad website |
| 1 | 1 | 0 | Unknown | [Learning_Idris](https://github.com/michelrandahl/Learning_Idris)/561 | Collection of exercise solutions and example snippets from misc Idris tutorials and 'Type Driven Development'. |
| 1 | 0 | 0 | Unknown | [elba](https://github.com/ctford/elba)/562 | An Idris type provider for type-checked protocols. |
| 1 | 0 | 0 | Unknown | [type-driven-development](https://github.com/minhnhdo/type-driven-development)/563 | None |
| 1 | 0 | 0 | Unknown | [advent_of_code_2017](https://github.com/Jell/advent_of_code_2017)/564 | None |
| 1 | 1 | 0 | Unknown | [IdrisSudoku](https://github.com/Vizaxo/IdrisSudoku)/565 | A simple sudoku solver written in idris to teach myself about using dependent types. |
| 1 | 0 | 0 | Unknown | [Idris-Blockchain](https://github.com/sciadopitys/Idris-Blockchain)/566 | None |
| 1 | 1 | 1 | Unknown | [simit](https://github.com/trsutton/simit)/567 | None |
| 1 | 0 | 0 | Unknown | [tdd-idris-book-exercises](https://github.com/antuneza/tdd-idris-book-exercises)/568 | Solutions to Exercises in Type-Driven Development with Idris |
| 1 | 0 | 0 | Unknown | [Algebra](https://github.com/ssbothwell/Algebra)/569 | Proving algebraic properties with Idris |
| 1 | 0 | 0 | Unknown | [idris-anagram](https://github.com/KeenS/idris-anagram)/570 | None |
| 1 | 0 | 0 | Unknown | [w-types](https://github.com/idris-industry/w-types)/571 | W types or well founded trees |
| 1 | 1 | 0 | Unknown | [programming-problems-in-idris](https://github.com/jameshfisher/programming-problems-in-idris)/572 | Problems from http://adriann.github.io/programming_problems.html, solutions using Idris |
| 1 | 0 | 0 | Unknown | [nosh](https://github.com/PolyglotSymposium/nosh)/573 | Nope syntax language hosting Semacrolon macro language preprocessing for Happle functional language |
| 1 | 0 | 0 | Unknown | [idris-playthings](https://github.com/marcusklaas/idris-playthings)/574 | None |
| 1 | 0 | 0 | Unknown | [tdd-idris_wjd](https://github.com/williamdemeo/tdd-idris_wjd)/575 | Notes and Exercises from the book "Type-Driven Development with Idris" |
| 1 | 0 | 0 | Unknown | [epidrin](https://github.com/ilya-klyuchnikov/epidrin)/576 | None |
| 1 | 0 | 0 | Unknown | [idris-gpd](https://github.com/typedefs/idris-gpd)/577 | Generic Packet Descriptions in Idris |
| 1 | 0 | 0 | Unknown | [idris-okasaki-pfds](https://github.com/ska80/idris-okasaki-pfds)/578 | "Purely Functional Data Structures", by Chris Okasaki |
| 1 | 0 | 0 | Unknown | [idris](https://github.com/0918nobita/idris)/579 | Idris code examples |
| 1 | 0 | 0 | Unknown | [ep-idris](https://github.com/casvdrest/ep-idris)/580 | None |
| 1 | 0 | 0 | Unknown | [idris-bench](https://github.com/andrevidela/idris-bench)/581 | None |
| 1 | 0 | 0 | Unknown | [HomotopyTypeTheory](https://github.com/KenyC/HomotopyTypeTheory)/582 | Some definitions and propositions of Homotopy Type Theory |
| 1 | 0 | 0 | Unknown | [typed-counterpoint](https://github.com/aaronallen8455/typed-counterpoint)/583 | If your composition doesn't follow the counterpoint rules, the compiler rejects it! |
| 1 | 0 | 0 | Unknown | [Cellular](https://github.com/ssbothwell/Cellular)/584 | Cellular Automata experiments in Idris |
| 1 | 0 | 1 | Unknown | [idris-time](https://github.com/gdevanla/idris-time)/585 | A port of GHC time library to Idris |
| 1 | 0 | 0 | Unknown | [Proofs](https://github.com/skykanin/Proofs)/586 | Collection of formal proofs |
| 1 | 1 | 0 | Unknown | [QFeldspar-Idris](https://github.com/shayan-najd/QFeldspar-Idris)/587 | A port of QFeldspar to Idris |
| 1 | 0 | 0 | Unknown | [Anvil](https://github.com/nv-vn/Anvil)/588 | A safe package manager in Idris |
| 1 | 0 | 0 | Unknown | [idris-stuff](https://github.com/defanor/idris-stuff)/589 | None |
| 1 | 0 | 0 | Unknown | [alice-in-puzzleland](https://github.com/yurrriq/alice-in-puzzleland)/590 | None |
| 1 | 0 | 0 | Unknown | [interruption](https://github.com/evanrinehart/interruption)/591 | None |
| 1 | 2 | 0 | Unknown | [idris-fizzbuzz](https://github.com/tomphp/idris-fizzbuzz)/592 | An attempt to write a proven fizzbuzz implementation in Idris |
| 1 | 0 | 0 | Unknown | [idris-tdd](https://github.com/trinary/idris-tdd)/593 | Examples and exercises from "Type Driven Development with Idris" |
| 1 | 0 | 0 | Unknown | [minihaskell-idris](https://github.com/PolyglotSymposium/minihaskell-idris)/594 | A port of plzoo's minihaskell in Idris |
| 1 | 0 | 0 | Unknown | [ipm](https://github.com/mmn80/ipm)/595 | None |
| 1 | 0 | 0 | Unknown | [espris](https://github.com/aktowns/espris)/596 | idris ported to the esp32 |
| 1 | 0 | 0 | Unknown | [IshiiSan_Galois_Idris](https://github.com/righ1113/IshiiSan_Galois_Idris)/597 | 『ガロア理論の頂を踏む』読書ノート |
| 1 | 1 | 0 | Unknown | [singularity](https://github.com/byee4/singularity)/598 | Singularity files, mostly just pulling from docker |
| 1 | 0 | 0 | Unknown | [201811-munihac](https://github.com/janschultecom/201811-munihac)/599 | None |
| 1 | 0 | 0 | Unknown | [flexidisc](https://github.com/berewt/flexidisc)/600 | Typesafe extensible records (and more) for Idris. |
| 1 | 0 | 0 | 5 years ago | [idris-classdata](https://github.com/runKleisli/idris-classdata)/601 | Using type classes like data types |
| 1 | 0 | 0 | 5 years ago | [qualitative-order](https://github.com/shlevy/qualitative-order)/602 | Mathematical formalism of qualitatively ordered types |
| 1 | 0 | 0 | 4 years ago | [pong](https://github.com/not-fl3/pong)/603 | The most correct pong ever |
| 1 | 0 | 0 | 4 years ago | [idris-type-driven-development](https://github.com/Chouffe/idris-type-driven-development)/604 | Idris Playground (Book Type Driven Development) |
| 1 | 0 | 0 | 4 years ago | [game-of-life](https://github.com/artemohanjanyan/game-of-life)/605 | None |
| 1 | 0 | 0 | 2 years ago | [idris-talk](https://github.com/HenryS1/idris-talk)/606 | Dependent Types with Idris Lambda Luminaries talk 9 October 2017 |
| 1 | 0 | 0 | 1 year, 5 months ago | [jimi](https://github.com/ilya-klyuchnikov/jimi)/607 | None |
| 1 | 0 | 0 | 2 years ago | [hello-idris](https://github.com/bor0/hello-idris)/608 | A WordPress plugin written in Idris |
| 1 | 0 | 0 | 1 year, 9 months ago | [idris-http](https://github.com/abailly/idris-http)/609 | An HTTP server in Idris2 |
| 1 | 0 | 0 | 1 year, 1 month ago | [codenames](https://github.com/gergoerdi/codenames)/610 | Grid generator for Codenames & Codenames Duet |
| 1 | 0 | 0 | 7 months ago | [ECC](https://github.com/ionathanch/ECC)/611 | Various models of Luo's Extended Calculus of Constructions. |
| 1 | 0 | 0 | a month ago | [idris2-toolkit](https://github.com/jfdm/idris2-toolkit)/612 | I collection of things I use in Idris2 that I dump into private projects to avoid dependency hell. |
| 1 | 0 | 0 | 3 months ago | [iteree-parser](https://github.com/Jeremy-Stafford/iteree-parser)/613 | An iteree-based parser library in Idris. |
| 1 | 0 | 0 | 4 years ago | [idris-examples](https://github.com/janschultecom/idris-examples)/614 | None |
| 1 | 0 | 0 | 5 years ago | [chu_shogi_server](https://github.com/colin-adams/chu_shogi_server)/615 | Implementation of a Chu Shogi server in Idris that is supposed to be correctly proven against a specification of the rules |
| 1 | 0 | 0 | 2 years ago | [edda](https://github.com/jfdm/edda)/616 | A processing engine for documents written in markdown-like languages. |
| 1 | 0 | 0 | 3 years ago | [FiniteEnum](https://github.com/berewt/FiniteEnum)/617 | Enumeration of finite types in Idris |
| 1 | 1 | 0 | 4 years ago | [idris-book](https://github.com/gbasler/idris-book)/618 | Exercises form Type-Driven Programming in Idris |
| 1 | 0 | 0 | 3 years ago | [AoC2017](https://github.com/tscholak/AoC2017)/619 | None |
| 1 | 0 | 0 | 10 months ago | [idris-effekt](https://github.com/b-studios/idris-effekt)/620 | Delimited control effects in Idris |
| 1 | 0 | 0 | 2 years ago | [nineninths](https://github.com/Kazark/nineninths)/621 | Proof in Idris of the theorem that 1 = 0.999... |
| 1 | 0 | 0 | 2 years ago | [dctp](https://github.com/tauoverpi/dctp)/622 | Functional Reactive Programming library |
| 1 | 0 | 0 | 3 months ago | [48scheme.idr](https://github.com/1inguini/48scheme.idr)/623 | r5rs subset in Idris |
| 1 | 0 | 0 | 6 days ago | [idris2-comonad](https://github.com/stefan-hoeck/idris2-comonad)/624 | None |
| 1 | 0 | 0 | 5 years ago | [demo-code](https://github.com/bixuanzju/demo-code)/625 | demo code for Idirs meetup |
| 1 | 0 | 0 | 5 years ago | [idris-meap](https://github.com/nabilhassein/idris-meap)/626 | Exercises from Edwin Brady's forthcoming "Type-Driven Development with Idris" through the Manning Early Access Program |
| 1 | 0 | 0 | 5 years ago | [idris-data-structures](https://github.com/amal029/idris-data-structures)/627 | Data structures implemented in Idris |
| 1 | 0 | 0 | 4 years ago | [THH](https://github.com/ltics/THH)/628 | explore the core TS specs |
| 1 | 0 | 0 | 7 years ago | [cpdt-idris](https://github.com/domdere/cpdt-idris)/629 | Code-A-Long for Certified Programming with Dependent Types [Idris] |
| 1 | 0 | 0 | 4 years ago | [geometry-explore](https://github.com/alexFrankfurt/geometry-explore)/630 | Geometry stuff with Idris. |
| 1 | 0 | 0 | 3 years ago | [idris-roman-numerals](https://github.com/chrisriess/idris-roman-numerals)/631 | Presentation and code from the Munich Lambda meetup on 20 Nov 2017 |
| 1 | 1 | 0 | 5 years ago | [idris-map](https://github.com/athanclark/idris-map)/632 | Simple Data.Map port to Idris |
| 1 | 0 | 0 | 3 years ago | [cospanProc](https://github.com/jameshaydon/cospanProc)/633 | Composing coroutines via decorated cospans |
| 1 | 0 | 0 | 2 years ago | [kolgut-api](https://github.com/janschultecom/kolgut-api)/634 | Schema-safe http api using Idris+Rust |
| 1 | 0 | 1 | 2 years ago | [idris-mongo](https://github.com/unalos/idris-mongo)/635 | Idris bindings to the C mongodb connector |
| 1 | 0 | 0 | 1 year, 7 months ago | [IdrisBookExercises](https://github.com/ssbothwell/IdrisBookExercises)/636 | Exercises for Type Driven Development With Idris |
| 1 | 1 | 0 | 2 years ago | [Dependently_Typed_Einsum](https://github.com/bgavran/Dependently_Typed_Einsum)/637 | WIP |
| 1 | 0 | 0 | 6 months ago | [blockchain](https://github.com/Icelandjack/blockchain)/638 | None |
| 1 | 0 | 0 | 3 years ago | [bulls-and-cows](https://github.com/dmalikov/bulls-and-cows)/639 | Implementation of Bulls and Cows game |
| 1 | 0 | 0 | 2 years ago | [Sql](https://github.com/leon-vv/Sql)/640 | Idris Sql package, type safe queries |
| 1 | 0 | 0 | 2 years ago | [idris](https://github.com/hackle/idris)/641 | Idris exercises |
| 1 | 0 | 0 | 3 years ago | [solutions-tddi](https://github.com/bixuanzju/solutions-tddi)/642 | Being the solutions to the exercises contained in the book "Type-Driven Development with Idris" |
| 1 | 0 | 0 | 5 years ago | [CS1](https://github.com/codycollins/CS1)/643 | None |
| 1 | 0 | 0 | 5 years ago | [Timespace](https://github.com/laurmcarter/Timespace)/644 | Exploration of tradeoff between time and space under isomorphisms. |
| 1 | 0 | 0 | 7 years ago | [idris-toy](https://github.com/seagull-kamome/idris-toy)/645 | toy for idris program language |
| 1 | 2 | 0 | 6 years ago | [idris-json-rpc](https://github.com/defanor/idris-json-rpc)/646 | JSON-RPC 2.0 in Idris |
| 1 | 0 | 0 | 3 years ago | [idris-learn](https://github.com/gostrider/idris-learn)/647 | Learning Idris  |
| 1 | 0 | 0 | 4 years ago | [idris-a-mazing](https://github.com/ItsLastDay/idris-a-mazing)/648 | Exam project for "Programming with dependent types using Idris" course |
| 1 | 0 | 0 | 3 years ago | [idris-async](https://github.com/Risto-Stevcev/idris-async)/649 | Higher-level abstractions for asynchronous code in idris |
| 1 | 0 | 0 | 1 year, 4 days ago | [vzipper](https://github.com/homotopic-tech/vzipper)/650 | Fixed length zipper in Idris. |
| 0 | 0 | 0 | 6 years ago | [dbus-idris](https://github.com/projedi/dbus-idris)/651 | None |
| 0 | 0 | 0 | 6 years ago | [blob-wars](https://github.com/dillonhuff/blob-wars)/652 | blob wars in idris |
| 0 | 0 | 0 | 6 years ago | [IdrisDemo](https://github.com/walkie/IdrisDemo)/653 | A brief example-based introduction to Idris. |
| 0 | 0 | 0 | 5 years ago | [Lab11.12.2015](https://github.com/BravoEch/Lab11.12.2015)/654 | Lab group work. |
| 0 | 0 | 0 | 5 years ago | [microKandris](https://github.com/jmitchell/microKandris)/655 | microKanren in Idris |
| 0 | 0 | 0 | 3 years ago | [semantics-of-programming-languages](https://github.com/lagenorhynque/semantics-of-programming-languages)/656 | Study notes on semantics of programming languages & theorem proving |
| 0 | 0 | 0 | 5 years ago | [griffincs1](https://github.com/williamwalker2/griffincs1)/657 | Whole CS1 directory |
| 0 | 0 | 0 | 5 years ago | [cs1](https://github.com/CrzyMonkeyNinja/cs1)/658 | None |
| 0 | 0 | 0 | 4 years ago | [l2idris](https://github.com/mat8913/l2idris)/659 | A bunch of code that I'm writing to learn Idris |
| 0 | 0 | 0 | 5 years ago | [devour](https://github.com/faineance/devour)/660 | Monadic Parser combinator μlibrary |
| 0 | 0 | 0 | 5 years ago | [meno-slave-proof](https://github.com/Risto-Stevcev/meno-slave-proof)/661 | My first, mostly lame proof in Idris, based on the puzzle given by Socrates to one of Meno's slaves in "Meno" by Plato |
| 0 | 0 | 0 | 7 years ago | [X11](https://github.com/paulkoerbitz/X11)/662 | X11 bindings for Idris |
| 0 | 0 | 0 | 7 years ago | [turbo_types_presentation](https://github.com/jedesah/turbo_types_presentation)/663 | A collection of code samples that go with my Turbo Types presentation |
| 0 | 0 | 0 | 5 years ago | [cs1113](https://github.com/jmh7xe/cs1113)/664 | None |
| 0 | 0 | 0 | 3 years ago | [idris_book](https://github.com/cybergrind/idris_book)/665 | exercises from https://www.manning.com/books/type-driven-development-with-idris |
| 0 | 0 | 0 | 3 years ago | [HS_ruleset](https://github.com/andrevidela/HS_ruleset)/666 | None |
| 0 | 0 | 0 | 3 years ago | [DynIdris](https://github.com/zaoqi/DynIdris)/667 | Idris模拟动态类型 |
| 0 | 0 | 0 | 1 year, 3 months ago | [PrivGen-Rep](https://github.com/BoujdadFz/PrivGen-Rep)/668 | None |
| 0 | 0 | 0 | 3 years ago | [TypeDD-Idris](https://github.com/RomanKapitonov/TypeDD-Idris)/669 | None |
| 0 | 0 | 0 | 4 years ago | [idris-ratio-calc](https://github.com/rouanth/idris-ratio-calc)/670 | Calculator for real numbers |
| 0 | 0 | 0 | 4 years ago | [idris-book](https://github.com/balajisivaraman/idris-book)/671 | Working through Type Driven Development In Idris Exercises |
| 0 | 0 | 0 | 4 years ago | [idr](https://github.com/shij-hsu/idr)/672 | idr习题 |
| 0 | 0 | 0 | 4 years ago | [type-driven-development-with-idris](https://github.com/chendrix/type-driven-development-with-idris)/673 | None |
| 0 | 1 | 0 | 4 years ago | [dragon](https://github.com/abinr/dragon)/674 | Chapter Exercises for Type-Driven Development Book |
| 0 | 0 | 0 | 4 years ago | [soundcheck](https://github.com/aaron-harris/soundcheck)/675 | A basic testing library for Idris, along the lines of QuickCheck |
| 0 | 0 | 0 | 3 years ago | [idris-jserror](https://github.com/Risto-Stevcev/idris-jserror)/676 | The javascript error type in idris |
| 0 | 0 | 0 | 4 years ago | [learning-idris](https://github.com/Nevon/learning-idris)/677 | None |
| 0 | 0 | 0 | 3 years ago | [idris-stache](https://github.com/BartAdv/idris-stache)/678 | Mustache parser implementation for Idris, basing on Haskell 'stache' |
| 0 | 0 | 0 | 4 years ago | [tdd-idris](https://github.com/raineorshine/tdd-idris)/679 | None |
| 0 | 0 | 0 | 2 years ago | [idris-chain](https://github.com/rpeszek/idris-chain)/680 | Dependently typed blockchain experiments in Idris |
| 0 | 0 | 0 | 3 years ago | [tic-tac-toe](https://github.com/JD95/tic-tac-toe)/681 | None |
| 0 | 0 | 0 | 2 years ago | [modern-compiler-implementation-in-ml](https://github.com/KPCCoiL/modern-compiler-implementation-in-ml)/682 | implementation and exercises of "Modern Compiler Implementation in ML" |
| 0 | 0 | 0 | 1 year, 4 months ago | [idris-exercises](https://github.com/tetrapharmakon/idris-exercises)/683 | None |
| 0 | 0 | 0 | 1 year, 25 days ago | [Lattices-in-Idris](https://github.com/anotherArka/Lattices-in-Idris)/684 | Trying to prove Knaster-Tarski theorem in Idris |
| 0 | 0 | 0 | 2 years ago | [scratch](https://github.com/roycrippen/scratch)/685 | Example Idris project structure for a creating a library. |
| 0 | 0 | 0 | 2 years ago | [sheeps](https://github.com/andrevidela/sheeps)/686 | None |
| 0 | 0 | 0 | 2 years ago | [sf-idris](https://github.com/rwblickhan/sf-idris)/687 | 🐉 Software Foundations done up in Idris |
| 0 | 0 | 0 | 2 years ago | [es-idris](https://github.com/codehag/es-idris)/688 | An experimental and rather direct ECMAScript implementation in Idris |
| 0 | 0 | 0 | 2 months ago | [dependent-containers](https://github.com/quinquice/dependent-containers)/689 | Weird and Absurd Data Structures, Written in Idris. |
| 0 | 0 | 0 | 1 year, 4 months ago | [fgli](https://github.com/doyougnu/fgli)/690 | A reimplementation of Erwig's fgl library in Idris (1) |
| 0 | 0 | 0 | 1 year, 6 months ago | [uwe](https://github.com/eayus/uwe)/691 | Uwe, a purely functional package manager written in Idris |
| 0 | 0 | 0 | 1 year, 8 months ago | [idris-calc](https://github.com/1inguini/idris-calc)/692 | idrisの練習、計算機 |
| 0 | 0 | 0 | 1 year, 9 months ago | [ProperMonads-Idris](https://github.com/LorenzoPerticone/ProperMonads-Idris)/693 | Monad instances quite similar to the Haskell standard library, with a formal verification of all axioms |
| 0 | 0 | 0 | 1 year, 7 months ago | [controlST](https://github.com/vfrinken/controlST)/694 | None |
| 0 | 0 | 0 | 4 months ago | [BiNat](https://github.com/SekiT/BiNat)/695 | Binary representation of natural numbers in Idris |
| 0 | 0 | 0 | 3 months ago | [idris-diaries](https://github.com/tarik-ozkanli/idris-diaries)/696 | None |
| 0 | 0 | 0 | 1 year, 29 days ago | [2020-idris](https://github.com/karlviik/2020-idris)/697 | None |
| 0 | 0 | 0 | 8 months ago | [WTInterp](https://github.com/bbarker/WTInterp)/698 | Well typed interpreter from Idris 2 docs, with Inigo packaging |
| 0 | 0 | 0 | 4 months ago | [idris2splitmix](https://github.com/Z-snails/idris2splitmix)/699 | Splitmix implementation in Idris (2) |
| 0 | 0 | 0 | 4 months ago | [TAPL-Idris](https://github.com/alebahn/TAPL-Idris)/700 | Implementing examples from Types and Programming languages in Idris |
| 0 | 0 | 0 | Unknown | [TAPL-Idris](https://github.com/alebahn/TAPL-Idris)/701 | Implementing examples from Types and Programming languages in Idris |
| 0 | 0 | 0 | Unknown | [idris2splitmix](https://github.com/Z-snails/idris2splitmix)/702 | Splitmix implementation in Idris (2) |
| 0 | 0 | 0 | Unknown | [idris2-skeletons](https://github.com/CodingCellist/idris2-skeletons)/703 | An implementation of various parallel programming patterns (aka. skeletons) in Idris2 |
| 0 | 0 | 0 | Unknown | [provable_fizz_buzz](https://github.com/magpie-engineering/provable_fizz_buzz)/704 | A formal proof for fizz buzz |
| 0 | 0 | 0 | Unknown | [idris-crypto-types](https://github.com/silky/idris-crypto-types)/705 | Types for crypto |
| 0 | 0 | 0 | Unknown | [idris-segments](https://github.com/artuuge/idris-segments)/706 | None |
| 0 | 0 | 0 | Unknown | [Echologie.github.io](https://github.com/Echologie/Echologie.github.io)/707 | None |
| 0 | 0 | 0 | Unknown | [idris-AES](https://github.com/karshan/idris-AES)/708 | None |
| 0 | 0 | 0 | Unknown | [coerceo](https://github.com/yacinehmito/coerceo)/709 | Base repo for the Coerceo board game challenge |
| 0 | 0 | 0 | Unknown | [cs1113-fall15](https://github.com/qter9692/cs1113-fall15)/710 | None |
| 0 | 0 | 0 | Unknown | [hcj-idr](https://github.com/jeffersoncarpenter/hcj-idr)/711 | None |
| 0 | 0 | 0 | Unknown | [BullsNCows](https://github.com/kokarem1/BullsNCows)/712 | BullsNCows Game (Idris) |
| 0 | 0 | 0 | Unknown | [idris-playground](https://github.com/projedi/idris-playground)/713 | None |
| 0 | 0 | 0 | Unknown | [idris_playground](https://github.com/colinbull/idris_playground)/714 | Repository of my adventures with idris |
| 0 | 0 | 0 | Unknown | [idris-discrete](https://github.com/bascott/idris-discrete)/715 | None |
| 0 | 0 | 0 | Unknown | [cs1](https://github.com/shell50/cs1)/716 | None |
| 0 | 0 | 0 | Unknown | [Cs1](https://github.com/Bonnycastle/Cs1)/717 | None |
| 0 | 0 | 0 | Unknown | [cs1](https://github.com/sophjk/cs1)/718 | None |
| 0 | 0 | 0 | Unknown | [cs1](https://github.com/dmc2dn/cs1)/719 | None |
| 0 | 0 | 0 | Unknown | [cs1113](https://github.com/heidijun97/cs1113)/720 | None |
| 0 | 0 | 0 | Unknown | [dependent-types-talk](https://github.com/Warbo/dependent-types-talk)/721 | Mirror of http://chriswarbo.net/git/dependent-types-talk |
| 0 | 0 | 0 | Unknown | [idrisjava-prototype-to-ffi-interface](https://github.com/bgaster/idrisjava-prototype-to-ffi-interface)/722 | Simple program to take a Java method prototype and generate IdrisJava FFI interface |
| 0 | 0 | 0 | Unknown | [Idris](https://github.com/StrangeLoopCodingDojo/Idris)/723 | Idris |
| 0 | 0 | 0 | Unknown | [DIY-Idris-Library](https://github.com/e-zou/DIY-Idris-Library)/724 | This library took a semester in school to make. It includes basic functions such as adding/ subtracting bits and bytes. |
| 0 | 0 | 0 | Unknown | [tdd-with-idris-exercises](https://github.com/originerd/tdd-with-idris-exercises)/725 | Solutions to exercises of Type-Driven Development with Idris |
| 0 | 0 | 0 | Unknown | [idris-book-exercises](https://github.com/mynomoto/idris-book-exercises)/726 | None |
| 0 | 0 | 0 | Unknown | [tdd-book](https://github.com/tsdh/tdd-book)/727 | Exercises from Type-Driven Development with Idris |
| 0 | 0 | 0 | Unknown | [st-random](https://github.com/clayrat/st-random)/728 | Control.ST.Random |
| 0 | 0 | 0 | Unknown | [i64jasm](https://github.com/TartanLlama/i64jasm)/729 | An x64 JIT assembler |
| 0 | 0 | 0 | Unknown | [practice-idris](https://github.com/w0mTea/practice-idris)/730 | Some practice projects with Idris |
| 0 | 0 | 0 | Unknown | [tictactoe](https://github.com/scotthellman/tictactoe)/731 | None |
| 0 | 0 | 0 | Unknown | [LearningIdris](https://github.com/PhilAndrew/LearningIdris)/732 | Following the Idris language book |
| 0 | 0 | 0 | Unknown | [idris-dependent-list-items](https://github.com/codygman/idris-dependent-list-items)/733 | None |
| 0 | 0 | 0 | Unknown | [tdd-with-idris](https://github.com/arturaz/tdd-with-idris)/734 | Excercises for the book Type-Driven Development with Idris by Edwin Brady |
| 0 | 0 | 0 | Unknown | [idris-fun](https://github.com/sleexyz/idris-fun)/735 | None |
| 0 | 0 | 0 | Unknown | [nerodu](https://github.com/PolyglotSymposium/nerodu)/736 | set("unordered") = {'n', 'e', 'r', 'o', 'd', 'u'} |
| 0 | 0 | 0 | Unknown | [parseit](https://github.com/hardvain/parseit)/737 | A parser combinator library written in Idris |
| 0 | 0 | 0 | Unknown | [Advent-of-Code-2017](https://github.com/iasoon/Advent-of-Code-2017)/738 | None |
| 0 | 0 | 0 | Unknown | [containersandbox](https://github.com/ericbaer/containersandbox)/739 | Random data structures in Idris |
| 0 | 0 | 0 | Unknown | [idris-projects](https://github.com/ArulselvanMadhavan/idris-projects)/740 | Idris Projects |
| 0 | 0 | 0 | Unknown | [idris-book](https://github.com/belamenso/idris-book)/741 | Notes and exercises from "Type-Driven Development with Idris" |
| 0 | 0 | 0 | Unknown | [type-level-sudoku](https://github.com/MightyAlex200/type-level-sudoku)/742 | Invalid Sudoku solutions are a type error |
| 0 | 0 | 0 | Unknown | [idris-btree](https://github.com/KeenS/idris-btree)/743 | None |
| 0 | 0 | 0 | Unknown | [idris-contrib](https://github.com/shmish111/idris-contrib)/744 | Standalone clone of idris contrib library |
| 0 | 0 | 0 | Unknown | [Idris-Fraction](https://github.com/stop-cran/Idris-Fraction)/745 | A fraction view for Nat and some its properties |
| 0 | 0 | 0 | Unknown | [idris-lambda-apigateway](https://github.com/hackle/idris-lambda-apigateway)/746 | None |
| 0 | 0 | 0 | Unknown | [read-vector](https://github.com/rcook/read-vector)/747 | Practical example of I/O combined with dependent types in Idris |
| 0 | 0 | 0 | Unknown | [fingertree](https://github.com/klausnat/fingertree)/748 | fingertree: Generic finger-tree structure, with example instances. Idris |
| 0 | 0 | 0 | Unknown | [parallel-fp](https://github.com/nkabrown/parallel-fp)/749 | Coding through COMP 312: Parallel and Sequential Algorithms in Idris |
| 0 | 1 | 0 | Unknown | [DDD-and-Dependent-Types](https://github.com/martinsson/DDD-and-Dependent-Types)/750 | Explorations of dependent types used for domain driven design |
| 0 | 0 | 0 | Unknown | [learning-idris](https://github.com/BlackCapCoder/learning-idris)/751 | Code written while learning the Idris language, from the perspective of a Haskeller |
| 0 | 0 | 0 | Unknown | [battle_dev_11](https://github.com/Shakadak/battle_dev_11)/752 | None |
| 0 | 0 | 0 | Unknown | [idris-exercises](https://github.com/ssanj/idris-exercises)/753 | Exercises from Type-Driven Development with Idris |
| 0 | 0 | 0 | Unknown | [idris-electron-react-scaffold](https://github.com/jheiling/idris-electron-react-scaffold)/754 | Electron-React scaffold for Idris |
| 0 | 0 | 0 | Unknown | [idris-bits](https://github.com/defndaines/idris-bits)/755 | Miscellaneous Idris Code |
| 0 | 0 | 0 | Unknown | [idris-cli-timer](https://github.com/robkorn/idris-cli-timer)/756 | Simple CLI timer written in Idris. |
| 0 | 0 | 0 | Unknown | [cct-exercises](https://github.com/mstn/cct-exercises)/757 | Exercises in Computational Category Theory from classical textbooks using idris-ct |
| 0 | 0 | 0 | Unknown | [grocery](https://github.com/dkeehl/grocery)/758 | None |
| 0 | 0 | 0 | Unknown | [software-foundations](https://github.com/erdeszt/software-foundations)/759 | Software foundations in Idris & Coq |
| 0 | 0 | 0 | Unknown | [tdd_ex](https://github.com/Ablach/tdd_ex)/760 | None |
| 0 | 0 | 0 | Unknown | [PRSA](https://github.com/clayrat/PRSA)/761 | Proof-relevant separation algebras from Rouvoet et al |
| 0 | 0 | 0 | Unknown | [insta-code](https://github.com/pawelsawicz/insta-code)/762 | None |
| 0 | 0 | 0 | Unknown | [pfsm-to-dart-client](https://github.com/titan/pfsm-to-dart-client)/763 | None |
| 0 | 0 | 2 | Unknown | [idris-concur-core](https://github.com/bbarker/idris-concur-core)/764 | A currently experimental/WIP port of Concur to Idris2 |
| 0 | 0 | 0 | Unknown | [Idris2-issues](https://github.com/nicolabotta/Idris2-issues)/765 | Document issues that I have encountered in using Idris 2 |
| 0 | 0 | 0 | Unknown | [YART](https://github.com/MarkMarkyMarkus/YART)/766 | For educational purposes only |
| 0 | 0 | 0 | Unknown | [pfsm-to-nim-service2](https://github.com/titan/pfsm-to-nim-service2)/767 | None |
| 0 | 0 | 0 | Unknown | [idris-spb-assignment-1](https://github.com/4e6/idris-spb-assignment-1)/768 | None |
| 0 | 0 | 0 | Unknown | [ttfp](https://github.com/donovancrichton/ttfp)/769 | My working through Type Theory and Formal Proofs (Nederpelt and Geuvers) in Idris. |
| 0 | 0 | 0 | Unknown | [Idris](https://github.com/NidhiMadab/Idris)/770 | None |
| 0 | 0 | 0 | Unknown | [aoc](https://github.com/fitzgibbon/aoc)/771 | Advent of Code |
| 0 | 0 | 0 | Unknown | [idris-examples](https://github.com/scharris/idris-examples)/772 | None |
| 0 | 0 | 0 | Unknown | [rewrite](https://github.com/ShinKage/rewrite)/773 | Verified directed graph rewriting with Idris |
| 0 | 0 | 0 | Unknown | [ih](https://github.com/easafe/ih)/774 | roguelike game |
| 0 | 0 | 0 | Unknown | [Opinonion](https://github.com/SebJansen/Opinonion)/775 | None |
| 0 | 0 | 0 | Unknown | [Submissions-for-CS-1113](https://github.com/Galvanaci/Submissions-for-CS-1113)/776 | None |
| 0 | 0 | 0 | Unknown | [CS1](https://github.com/TaKo2019/CS1)/777 | CS1 Directory with all IDRIS and Python files |
| 0 | 0 | 0 | Unknown | [idris-scratchpad](https://github.com/joprice/idris-scratchpad)/778 | experiments with Idris |
| 0 | 0 | 0 | Unknown | [automata](https://github.com/TimRichter/automata)/779 | finite state .s.o. in idris |
| 0 | 0 | 0 | Unknown | [CS1113](https://github.com/SordFysh/CS1113)/780 | None |
| 0 | 0 | 0 | Unknown | [morphisms](https://github.com/defanor/morphisms)/781 | Isomorphisms, sections, retractions. With printing and parsing in mind. |
| 0 | 0 | 0 | Unknown | [Idris-benchmarks](https://github.com/harelfishbein/Idris-benchmarks)/782 | None |
| 0 | 0 | 2 | Unknown | [testable-propositions](https://github.com/david-christiansen/testable-propositions)/783 | Testable propositions - postulate them if they pass! |
| 0 | 0 | 0 | Unknown | [atom-language-idris-tests](https://github.com/archaeron/atom-language-idris-tests)/784 | None |
| 0 | 0 | 0 | Unknown | [idris-package-manager](https://github.com/Invisible-Rabbit-Hunter/idris-package-manager)/785 | An idris package manager |
| 0 | 0 | 0 | Unknown | [idris-playground](https://github.com/asmodehn/idris-playground)/786 | My private idris fun zone |
| 0 | 0 | 0 | Unknown | [IdrisExperiments](https://github.com/GambolingPangolin/IdrisExperiments)/787 | Fun stuff I made to learn Idris |
| 0 | 0 | 0 | Unknown | [foid](https://github.com/mattyw/foid)/788 | None |
| 0 | 0 | 0 | Unknown | [idris-book](https://github.com/DimaSamoz/idris-book)/789 | Code examples and exercises from Type-Driven Development by Edwin Brady |
| 0 | 0 | 0 | Unknown | [Idris-dev_4159](https://github.com/msmorgan/Idris-dev_4159)/790 | Demonstration of idris-lang/Idris-dev #4159 |
| 0 | 0 | 0 | Unknown | [blodwen](https://github.com/ziman/blodwen)/791 | None |
| 0 | 0 | 0 | Unknown | [trans-sem](https://github.com/iteloo/trans-sem)/792 | Implementation of transformational semantics in Idris |
| 0 | 0 | 0 | Unknown | [aoc](https://github.com/dpk/aoc)/793 | Advent of Code puzzles |
| 0 | 0 | 0 | Unknown | [discrete-math-idris](https://github.com/porglezomp-misc/discrete-math-idris)/794 | Using the dependently typed language Idris to prove things I run into while taking discrete math |
| 0 | 0 | 0 | Unknown | [PokerHands](https://github.com/as8709/PokerHands)/795 | Formally verified poker hand evaluation |
| 0 | 0 | 0 | Unknown | [tddi](https://github.com/johnchandlerburnham/tddi)/796 | Notes and exercises for Type-Driven Development with Idris by Edwin Brady |
| 0 | 0 | 0 | Unknown | [Arrows](https://github.com/spydr073/Arrows)/797 | Model multiset to multiset functions in Idris |
| 0 | 0 | 0 | Unknown | [idris](https://github.com/klausnat/idris)/798 | Type-Driven Development with Idris Book by Edwin Brady, Exercises |
| 0 | 0 | 0 | Unknown | [tdd-in-idris](https://github.com/vivanov/tdd-in-idris)/799 | My solutions for tasks from Type-Driven Development in Idris |
| 0 | 0 | 0 | Unknown | [IdrisTest](https://github.com/BryghtWords/IdrisTest)/800 | Testing library for Idris |
| 0 | 0 | 0 | 3 years ago | [idris_read_bytes_ct](https://github.com/xash/idris_read_bytes_ct)/801 | Read a file into List Bits8 during compile time in Idris |
| 0 | 0 | 0 | 3 years ago | [Euclidean-geometry](https://github.com/andrevidela/Euclidean-geometry)/802 | None |
| 0 | 0 | 0 | 2 years ago | [tdd-in-idris](https://github.com/vivanov/tdd-in-idris)/803 | My solutions for tasks from Type-Driven Development in Idris |
| 0 | 0 | 0 | 2 years ago | [idris-spring-boot](https://github.com/mmhelloworld/idris-spring-boot)/804 | Spring Boot for Idris |
| 0 | 0 | 0 | 2 years ago | [idris](https://github.com/klausnat/idris)/805 | Type-Driven Development with Idris Book by Edwin Brady, Exercises |
| 0 | 0 | 0 | 2 years ago | [IdrisTest](https://github.com/BryghtWords/IdrisTest)/806 | Testing library for Idris |
| 0 | 0 | 0 | 2 years ago | [Arrows](https://github.com/spydr073/Arrows)/807 | Model multiset to multiset functions in Idris |
| 0 | 0 | 2 | 1 year, 6 months ago | [idris-nt](https://github.com/bkushigian/idris-nt)/808 | idris number theory  |
| 0 | 0 | 0 | 1 year, 1 month ago | [Arith](https://github.com/AdamHarries/Arith)/809 | Blegh |
| 0 | 0 | 0 | 2 years ago | [type-driven-development-with-Idris](https://github.com/leetschau/type-driven-development-with-Idris)/810 | Notes and answers of the book "Type Driven Development with Idris" by Edwin Brady |
| 0 | 0 | 0 | 2 years ago | [programming-language-foundations-in-idris](https://github.com/minhnhdo/programming-language-foundations-in-idris)/811 | Programming language foundations in Idris |
| 0 | 0 | 0 | 1 year, 5 months ago | [idris-playground](https://github.com/remexre/idris-playground)/812 | None |
| 0 | 0 | 0 | 7 months ago | [enjoy-idris](https://github.com/severuscat/enjoy-idris)/813 | Some Idris tasks for Type Theory course. ITMO, 2019-2020 |
| 0 | 0 | 0 | 7 months ago | [pfsm-nim-test](https://github.com/titan/pfsm-nim-test)/814 | None |
| 0 | 0 | 0 | 2 months ago | [tiny-idris-program-synthesis](https://github.com/Ablach/tiny-idris-program-synthesis)/815 | None |
| 0 | 0 | 0 | 7 months ago | [oyster](https://github.com/timmyjose-compilers/oyster)/816 | A basic Parser-Combinator library in Idris. |
| 0 | 0 | 0 | 10 months ago | [csv-parser](https://github.com/wchresta/csv-parser)/817 | Simple CSV parser in Idris2 |
| 0 | 0 | 0 | 11 months ago | [Idris-exercises](https://github.com/neurogoo/Idris-exercises)/818 | None |
| 0 | 0 | 0 | 29 days ago | [idris2-dsa-gen](https://github.com/CodingCellist/idris2-dsa-gen)/819 | Generating Idris2 code based on Dependent State Automata diagrams. |
| 0 | 0 | 0 | a month ago | [two-pc-idr](https://github.com/davlum/two-pc-idr)/820 | Implementation of the Two Phase commit protocol in Idris |
| 0 | 0 | 0 | a month ago | [HoTT-Idris](https://github.com/ionathanch/HoTT-Idris)/821 | A mechanization of HoTT in Idris. |
| 0 | 0 | 0 | 24 days ago | [eucalyptus](https://github.com/danielwaterworth/eucalyptus)/822 | Hardware description language embedded in Idris 2 |
| 0 | 0 | 0 | 4 months ago | [hello_idris](https://github.com/Umu999/hello_idris)/823 | None |
| 0 | 0 | 0 | 11 days ago | [type-driven-development-with-idris](https://github.com/k-kom/type-driven-development-with-idris)/824 | None |
| 0 | 0 | 0 | 5 years ago | [polyglot-dabbling](https://github.com/PolyglotSymposium/polyglot-dabbling)/825 | The Polyglot Symposium dabbling in many languages |
| 0 | 0 | 0 | 6 years ago | [socketexp](https://github.com/davidpeklak/socketexp)/826 | Exploring sockets in idris |
| 0 | 0 | 0 | 6 years ago | [integers](https://github.com/forestbelton/integers)/827 | None |
| 0 | 0 | 0 | 5 years ago | [Idris-Tainted](https://github.com/RossMeikleham/Idris-Tainted)/828 | Implementation of the Tainted Monad in Idris |
| 0 | 0 | 0 | 5 years ago | [IdrisNotes](https://github.com/zenon/IdrisNotes)/829 | None |
| 0 | 0 | 0 | 5 years ago | [idris-learning-diary](https://github.com/jhegedus42/idris-learning-diary)/830 | Experimenting with fully dependent types. |
| 0 | 0 | 0 | 8 months ago | [dudo](https://github.com/pharpend/dudo)/831 | The game of Dudo implemented in Idris. |
| 0 | 0 | 0 | 5 years ago | [cs1113-fall15](https://github.com/fuwentan/cs1113-fall15)/832 | None |
| 0 | 1 | 0 | 5 years ago | [idris-canvas-drawing](https://github.com/TomShacham/idris-canvas-drawing)/833 | None |
| 0 | 0 | 0 | 5 years ago | [IdrisBasics](https://github.com/nguyenmv2/IdrisBasics)/834 | None |
| 0 | 0 | 0 | 7 years ago | [idris-compiler](https://github.com/cgswords/idris-compiler)/835 | A compiler written in Idris. We'll start with Scheme and see where it goes. |
| 0 | 0 | 0 | 7 years ago | [SimpleOptParse](https://github.com/relrod/SimpleOptParse)/836 | An extremely simple CLI option parser in Idris. Only a toy project, don't take it seriously. :) |
| 0 | 0 | 0 | 6 years ago | [dptexamples](https://github.com/tegansiobhan/dptexamples)/837 | None |
| 0 | 0 | 0 | 5 years ago | [tdd-talk](https://github.com/fthomas/tdd-talk)/838 | None |
| 0 | 0 | 0 | 5 years ago | [IdrisUnification](https://github.com/sammthomson/IdrisUnification)/839 | Playing around with "First-order Unification by Structural Recursion", McBride '03, J. Functional Programming |
| 0 | 0 | 0 | 4 years ago | [LearningIdris](https://github.com/chemouna/LearningIdris)/840 | None |
| 0 | 0 | 0 | 5 years ago | [tenniskata-idris](https://github.com/andredublin/tenniskata-idris)/841 | None |
| 0 | 0 | 0 | 4 years ago | [idris-book-listings](https://github.com/haskellcats/idris-book-listings)/842 | None |
| 0 | 0 | 0 | 4 years ago | [dailyprover](https://github.com/farrellm/dailyprover)/843 | Solutions to /r/dailyprover |
| 0 | 0 | 0 | 3 years ago | [idris-assert](https://github.com/Risto-Stevcev/idris-assert)/844 | A simple idris assertion library |
| 0 | 0 | 0 | 3 years ago | [idriscode](https://github.com/ujjwalrajput/idriscode)/845 | None |
| 0 | 0 | 0 | 3 years ago | [idris-twist](https://github.com/msmorgan/idris-twist)/846 | None |
| 0 | 0 | 0 | 3 years ago | [type-driven-dev-with-idris](https://github.com/northerner/type-driven-dev-with-idris)/847 | Exercises from Type-Driven Development with Idris by Edwin Brady  |
| 0 | 0 | 0 | 3 years ago | [Type_Driven_Dev-Idris](https://github.com/andrevidela/Type_Driven_Dev-Idris)/848 | repo for exercises of the TDD in Idris book |
| 0 | 0 | 0 | 3 years ago | [IdrisDiscovery](https://github.com/ToF-/IdrisDiscovery)/849 | A bag of mini katas to discover Idris |
| 0 | 0 | 0 | 4 years ago | [tdd-idris-exercises](https://github.com/seoh/tdd-idris-exercises)/850 | None |
| 0 | 0 | 0 | 3 years ago | [Matrix](https://github.com/kevinjcliao/Matrix)/851 | Library for playing around with type safe matrices in Idris. Well-trodden territory.  |
| 0 | 0 | 0 | 3 years ago | [idris-stuff](https://github.com/mariatsji/idris-stuff)/852 | personal idris projects |
| 0 | 0 | 0 | 2 years ago | [TDD-Idris-Exercises](https://github.com/nicklecompte/TDD-Idris-Exercises)/853 | notes + solutions to exercises from Edwin Brady's Type-Driven Development With Idris |
| 0 | 0 | 0 | 3 years ago | [idris-random-fail](https://github.com/camelpunch/idris-random-fail)/854 | A Control.ST.Random and FFI program that crashes Idris 1.3 |
| 0 | 0 | 0 | 3 years ago | [idris-callbacks-tests](https://github.com/thalerjonathan/idris-callbacks-tests)/855 | None |
| 0 | 0 | 0 | 2 years ago | [tableaux](https://github.com/fujiy/tableaux)/856 | None |
| 0 | 0 | 0 | 2 years ago | [cufp-2014](https://github.com/Jell/cufp-2014)/857 | None |
| 0 | 0 | 0 | 2 years ago | [fc](https://github.com/dwarfmaster/fc)/858 | Compiler for a small functionnal language |
| 0 | 0 | 0 | 1 year, 7 months ago | [fspp](https://github.com/Kazark/fspp)/859 | A sort of F# preprocessor hack |
| 0 | 0 | 0 | 2 years ago | [adventofcode2018](https://github.com/alrunner4/adventofcode2018)/860 | https://adventofcode.com/2018 |
| 0 | 0 | 0 | 2 years ago | [tdd](https://github.com/optician/tdd)/861 | None |
| 0 | 0 | 0 | 2 years ago | [Idris-Deps](https://github.com/chrrasmussen/Idris-Deps)/862 | List dependencies of an Idris project |
| 0 | 1 | 0 | 1 year, 9 months ago | [gcd](https://github.com/0xd34df00d/gcd)/863 | Euclidean algorithm, formally verified, provably correct |
| 0 | 0 | 0 | 1 year, 11 months ago | [idris-exercises](https://github.com/Nimor111/idris-exercises)/864 | Exercises and proofs while learning Idris |
| 0 | 0 | 0 | 1 year, 10 months ago | [idris-fist-steps](https://github.com/cattingcat/idris-fist-steps)/865 | None |
| 0 | 0 | 0 | 2 years ago | [idris-book](https://github.com/klangner/idris-book)/866 | Idris sandbox |
| 0 | 0 | 0 | 2 years ago | [2019-02-21-coding-for-students](https://github.com/janschultecom/2019-02-21-coding-for-students)/867 | None |
| 0 | 0 | 0 | 2 years ago | [GraphDB](https://github.com/spydr073/GraphDB)/868 | Dagger Category Database |
| 0 | 0 | 0 | 2 years ago | [P10](https://github.com/mortenm12/P10)/869 | None |
| 0 | 0 | 0 | 1 year, 7 months ago | [idris-group](https://github.com/remexre/idris-group)/870 | Stuff related to the UMN plseminar going through Type-Driven Development in Idris in Fall 2019. |
| 0 | 0 | 0 | 1 year, 5 months ago | [TypeDrivenDevIdrisExercises](https://github.com/afarnham/TypeDrivenDevIdrisExercises)/871 | Type Driven Development with Idris Exercises |
| 0 | 0 | 0 | 2 months ago | [idris-playground](https://github.com/jmgimeno/idris-playground)/872 | Playground for learning dependent type programming in Idris(2) |
| 0 | 0 | 0 | 2 months ago | [Maze-game](https://github.com/lucaszavalia/Maze-game)/873 | None |
| 0 | 0 | 0 | 6 months ago | [kladenets](https://github.com/SmiVan/kladenets)/874 | Music/Sound Library for Idris2, based on libsoundio/libsndfile bindings. |
| 0 | 0 | 0 | 2 months ago | [idris-playground](https://github.com/tbidne/idris-playground)/875 | None |
| 0 | 0 | 0 | 3 months ago | [idris-musings](https://github.com/gusbicalho/idris-musings)/876 | None |
| 0 | 0 | 0 | 3 months ago | [ijs](https://github.com/jjl/ijs)/877 | The missing javascript ffi stdlib for idris |
| 0 | 0 | 0 | 3 months ago | [idris-project](https://github.com/dannypsnl/idris-project)/878 | idris project template for myself |
| 0 | 0 | 0 | 4 months ago | [pfsm-to-nim-gateway](https://github.com/titan/pfsm-to-nim-gateway)/879 | None |
| 0 | 0 | 0 | 16 days ago | [type-driven-dev-idris](https://github.com/chespinoza/type-driven-dev-idris)/880 | None |
| 0 | 0 | 0 | 17 days ago | [regex-idris2](https://github.com/glyh/regex-idris2)/881 | Brzozowski Regex Derivatives library implemented in Idris2 |
| 0 | 0 | 0 | a month ago | [tcat](https://github.com/galtys/tcat)/882 | tcat |
| 0 | 0 | 0 | 8 days ago | [pgc-ufabc](https://github.com/LucasTornai/pgc-ufabc)/883 | None |
| 0 | 0 | 0 | 8 days ago | [idris2-buffered-channels](https://github.com/CodingCellist/idris2-buffered-channels)/884 | An attempt at implementing various channels for inter-process communication in Idris2 |
| 0 | 0 | 0 | 1 year, 10 months ago | [idrisgrouptheory](https://github.com/caldwellb/idrisgrouptheory)/885 | Implementation of basic group theory in Idris |
| 0 | 0 | 0 | 6 years ago | [idris-datalog](https://github.com/michaelpj/idris-datalog)/886 | None |
| 0 | 0 | 0 | 4 years ago | [tdd-idris-exercises](https://github.com/andredublin/tdd-idris-exercises)/887 | Exercise answers to Type Drive Development with Idris |
| 0 | 0 | 0 | 5 years ago | [cs1-real-repo-](https://github.com/SZwuxin/cs1-real-repo-)/888 | None |
| 0 | 0 | 0 | 5 years ago | [cs1113-fall15](https://github.com/czc3wa/cs1113-fall15)/889 | Intro to Programming |
| 0 | 0 | 0 | 5 years ago | [cs1](https://github.com/yossarian44/cs1)/890 | None |
| 0 | 0 | 0 | 5 years ago | [cs1](https://github.com/yolanda7975/cs1)/891 | None |
| 0 | 0 | 0 | 5 years ago | [homework](https://github.com/ckz5ac/homework)/892 | None |
| 0 | 0 | 0 | 5 years ago | [cs1](https://github.com/ckd111/cs1)/893 | None |
| 0 | 0 | 0 | 5 years ago | [arduino-painless](https://github.com/lives-group/arduino-painless)/894 | Painless Arduino programming through strongly typed embedded domain specific languages |
| 0 | 0 | 0 | 6 years ago | [Idris-sequences](https://github.com/treeowl/Idris-sequences)/895 | Experimental finger tree-based sequence implementations |
| 0 | 0 | 0 | 5 years ago | [OrbitSim](https://github.com/mankyKitty/OrbitSim)/896 | None |
| 0 | 0 | 0 | 5 years ago | [strangeloop2015_idris_dojo](https://github.com/karlhungus/strangeloop2015_idris_dojo)/897 | None |
| 0 | 0 | 0 | 6 years ago | [idris-sandbox](https://github.com/mproch/idris-sandbox)/898 | just a place to learn idris... |
| 0 | 0 | 0 | 4 years ago | [2048-idr](https://github.com/tsani/2048-idr)/899 | A 2048 clone in Idris |
| 0 | 0 | 0 | 3 years ago | [idris-book](https://github.com/chagasVinicius/idris-book)/900 | None |
| 0 | 0 | 0 | 4 years ago | [idrisexerc](https://github.com/stephen-lazaro/idrisexerc)/901 | None |
| 0 | 0 | 0 | 4 years ago | [tdd-idris](https://github.com/ericlobdell/tdd-idris)/902 | None |
| 0 | 0 | 0 | 4 years ago | [overmind](https://github.com/Raleigh-Foster/overmind)/903 | This is a dependent type development which serves as a sandbox for experimenting with artificial intelligence. |
| 0 | 0 | 0 | 3 years ago | [shenzhen-solitaire](https://github.com/dmit/shenzhen-solitaire)/904 | An implementation of Solitaire as seen in Shenzhen I/O |
| 0 | 0 | 0 | 3 years ago | [QuantumProgramming](https://github.com/GrandArchTemplar/QuantumProgramming)/905 | very simple project which consist of basic quantum calculation features and maybe smth else |
| 0 | 0 | 0 | 2 years ago | [idris_book_notes](https://github.com/Ryxai/idris_book_notes)/906 | Notes/Exercises from the book Type Driven Development in Idris |
| 0 | 0 | 0 | 3 years ago | [hendrix](https://github.com/ilya-klyuchnikov/hendrix)/907 | None |
| 0 | 0 | 0 | 3 years ago | [idris-casing](https://github.com/goodmind/idris-casing)/908 | None |
| 0 | 0 | 0 | 2 years ago | [idris-plm](https://github.com/brainrape/idris-plm)/909 | Principia Logico-Metaphysica |
| 0 | 1 | 0 | 3 years ago | [type-driven-lunch](https://github.com/jsoo1/type-driven-lunch)/910 | Learning idris at lunch |
| 0 | 0 | 0 | 3 years ago | [idris-book](https://github.com/chagasVinicius/idris-book)/911 | None |
| 0 | 0 | 0 | 4 years ago | [Idris_studies](https://github.com/DanielRrr/Idris_studies)/912 | None |
| 0 | 0 | 0 | 4 years ago | [2048-idr](https://github.com/tsani/2048-idr)/913 | A 2048 clone in Idris |
| 0 | 0 | 0 | 2 years ago | [permutations](https://github.com/archontophoenix/permutations)/914 | Some proofs in Coq (version 8.4p16) about permutations, including that the permutation relation is transitive. |
| 0 | 0 | 0 | 4 years ago | [IdrisExplorations](https://github.com/Crazycolorz5/IdrisExplorations)/915 | Just me testing out random code and concepts in Idris |
| 0 | 0 | 0 | 3 years ago | [idris-stuff](https://github.com/aweinstock314/idris-stuff)/916 | None |
| 0 | 0 | 0 | 4 years ago | [ibt](https://github.com/marcesquerra/ibt)/917 | Idris Build Tool |
| 0 | 0 | 0 | 3 years ago | [idris-nonempty](https://github.com/LightAndLight/idris-nonempty)/918 | Non-empty data structures |
| 0 | 0 | 0 | 3 years ago | [geb](https://github.com/yurrriq/geb)/919 | None |
| 0 | 0 | 0 | 3 years ago | [helloidris](https://github.com/jsalzbergedu/helloidris)/920 | A little repo to introduce myself to idris |
| 0 | 0 | 0 | 2 years ago | [verified-exact-real](https://github.com/jeroennoels/verified-exact-real)/921 | Verified exact real arithmetic in idris |
| 0 | 0 | 0 | 2 years ago | [idris-cg-dummy](https://github.com/doofin/idris-cg-dummy)/922 | None |
| 0 | 0 | 0 | 2 years ago | [graph](https://github.com/spydr073/graph)/923 | Inductive Graph Library |
| 0 | 1 | 0 | 2 years ago | [idris-examples](https://github.com/KokorinIlya/idris-examples)/924 | Some examples of programs with dependent types from Type Theory course in IFMO University. |
| 0 | 0 | 0 | 2 years ago | [idris-web-server](https://github.com/camelpunch/idris-web-server)/925 | A node-based web server library for Idris |
| 0 | 0 | 0 | 2 years ago | [filepath](https://github.com/Kazark/filepath)/926 | A sane, usable, cross-platform conceptual model for filepaths |
| 0 | 0 | 0 | 2 years ago | [versioning](https://github.com/Infinisil/versioning)/927 | None |
| 0 | 0 | 0 | 2 years ago | [idris-guessing-game](https://github.com/KeenS/idris-guessing-game)/928 | None |
| 0 | 0 | 0 | 2 years ago | [idris-stlc](https://github.com/Gwin73/idris-stlc)/929 | Verified typechecker and evaluator for Simply Typed Lamda Calculus (STLC) in Idris |
| 0 | 0 | 0 | 2 years ago | [idris-exercises](https://github.com/guilhermehas/idris-exercises)/930 | Solutions of the book Type Driven Development |
| 0 | 0 | 0 | 2 years ago | [idris-playground](https://github.com/widmogrod/idris-playground)/931 | Idris playground  |
| 0 | 0 | 0 | 2 years ago | [integers](https://github.com/0xd34df00d/integers)/932 | Look ma, I'm learning to count! |
| 0 | 0 | 0 | 2 years ago | [idris-four-in-a-row](https://github.com/Gwin73/idris-four-in-a-row)/933 | Text based Four In A Row in Idris |
| 0 | 0 | 0 | 1 year, 24 days ago | [PCF](https://github.com/normanrink/PCF)/934 | Development in Idris of standard meta-theory for a simply-typed lambda calculus with recursion. |
| 0 | 0 | 0 | 2 years ago | [transceiver-idr](https://github.com/sjsch/transceiver-idr)/935 | A reversible syntax combinator library for idris |
| 0 | 0 | 0 | 2 years ago | [software-foundations-in-idris](https://github.com/KeenS/software-foundations-in-idris)/936 | None |
| 0 | 0 | 0 | 2 years ago | [tdd-idris](https://github.com/curtisalexander/tdd-idris)/937 | Type Driven Development with Idris |
| 0 | 0 | 0 | Unknown | [tddi](https://github.com/bobbynarvy/tddi)/938 | Solutions to exercises from the book Type-Driven Development with Idris |
| 0 | 0 | 0 | Unknown | [iColor](https://github.com/marcesquerra/iColor)/939 | Terminal color for idris |
| 0 | 0 | 0 | Unknown | [advent-of-code-2020](https://github.com/AdamHarries/advent-of-code-2020)/940 | None |
| 0 | 0 | 0 | Unknown | [leetcode-idris](https://github.com/Smaug123/leetcode-idris)/941 | None |
| 0 | 0 | 0 | Unknown | [IdrisIntro](https://github.com/QuentinDuval/IdrisIntro)/942 | None |
| 0 | 0 | 0 | Unknown | [idris-from-the-docs](https://github.com/timmyjose-study/idris-from-the-docs)/943 | Learning Idris from the official docs |
| 0 | 0 | 0 | Unknown | [heavy-json](https://github.com/farmerzhang1/heavy-json)/944 | a json parser in idris for practices |
| 0 | 0 | 0 | Unknown | [idris-finite-sets](https://github.com/nicklecompte/idris-finite-sets)/945 | Tools for verified finite algebra / combinatorics in Idris |
| 0 | 0 | 0 | Unknown | [Genotype](https://github.com/SebJansen/Genotype)/946 | None |
| 0 | 0 | 0 | Unknown | [UPR-GRN](https://github.com/DaeKwan-Ko/UPR-GRN)/947 | None |
| 0 | 0 | 0 | Unknown | [alga-idris](https://github.com/b-hass/alga-idris)/948 | None |
| 0 | 0 | 0 | Unknown | [pfsm-nim-service2b-base](https://github.com/titan/pfsm-nim-service2b-base)/949 | None |
| 0 | 0 | 0 | Unknown | [pfsm-nim-base](https://github.com/titan/pfsm-nim-base)/950 | None |
| 0 | 0 | 0 | Unknown | [datapackris](https://github.com/refparo/datapackris)/951 | An EDSL for easily creating Minecraft datapacks |
| 0 | 0 | 0 | Unknown | [id-sixel](https://github.com/Kaiepi/id-sixel)/952 | Idris 2 libsixel bindings |
| 0 | 0 | 0 | Unknown | [ttfp-implementations](https://github.com/stefan-wullems/ttfp-implementations)/953 | Implementations following "Type Theory and Formal Proof: An Introduction". |
| 0 | 0 | 0 | Unknown | [tdd-solutions](https://github.com/asett0/tdd-solutions)/954 | My solutions to the exercises in Type Driven Development by Edwin Brady in Idris2 |
| 0 | 0 | 0 | Unknown | [gol](https://github.com/lmarburger/gol)/955 | Game of Life in Idris |
| 0 | 0 | 0 | Unknown | [ffiexp](https://github.com/davidpeklak/ffiexp)/956 | Experimenting with the idris FFI |
| 0 | 0 | 0 | Unknown | [idris-kats](https://github.com/briandipalma/idris-kats)/957 | Workshop on Idris |
| 0 | 0 | 0 | Unknown | [KataBankOCR](https://github.com/kevinmeredith/KataBankOCR)/958 | http://codingdojo.org/cgi-bin/index.pl?KataBankOCR w/ Idris |
| 0 | 0 | 0 | Unknown | [tddwi](https://github.com/d6y/tddwi)/959 | Type-driven development with Iris examples |
| 0 | 0 | 0 | Unknown | [AMysteryWord](https://github.com/kokarem1/AMysteryWord)/960 | A Mystery Word Game (Idris) |
| 0 | 0 | 0 | Unknown | [mapbox-gl-idris](https://github.com/lambdatoast/mapbox-gl-idris)/961 | None |
| 0 | 0 | 0 | Unknown | [2048.idr](https://github.com/Kraks/2048.idr)/962 | Game 2048 written in a language with dependent types. |
| 0 | 0 | 0 | Unknown | [struts](https://github.com/5outh/struts)/963 | Dependently typed music |
| 0 | 0 | 0 | Unknown | [cs1](https://github.com/runningchick/cs1)/964 | None |
| 0 | 0 | 0 | Unknown | [CS1-Repo](https://github.com/andolika2018/CS1-Repo)/965 | None |
| 0 | 0 | 0 | Unknown | [cs1](https://github.com/leahcox/cs1)/966 | All my/stuff/cs1 files |
| 0 | 0 | 0 | Unknown | [idris-ixlist](https://github.com/markandrus/idris-ixlist)/967 | A list indexed by its elements |
| 0 | 0 | 0 | Unknown | [learn-idris](https://github.com/timdestan/learn-idris)/968 | None |
| 0 | 0 | 0 | Unknown | [TDDWI-Exercises](https://github.com/deklanw/TDDWI-Exercises)/969 | Exercises from the Idris book |
| 0 | 0 | 0 | Unknown | [type-driven-development-with-idris-exercises](https://github.com/lazywithclass/type-driven-development-with-idris-exercises)/970 | My exercises for the book (https://www.manning.com/books/type-driven-development-with-idris) |
| 0 | 0 | 0 | Unknown | [duanwu](https://github.com/dkeehl/duanwu)/971 | A Scheme interpreter |
| 0 | 0 | 0 | Unknown | [typesIdris](https://github.com/stephen-lazaro/typesIdris)/972 | Doing Benjamin J Pierce's Types and Programming Languages in IDris |
| 0 | 0 | 0 | Unknown | [learn-idris](https://github.com/DjebbZ/learn-idris)/973 | Playground for learning Idris through "TDD with Idris" |
| 0 | 0 | 0 | Unknown | [idris_playground](https://github.com/cjen07/idris_playground)/974 | where to learn idris and apply it |
| 0 | 0 | 0 | Unknown | [idris-html](https://github.com/pierrebeaucamp/idris-html)/975 | An Idris library to interact with HTML |
| 0 | 0 | 0 | Unknown | [idris-playground](https://github.com/nebtrx/idris-playground)/976 | None |
| 0 | 0 | 1 | Unknown | [idris](https://github.com/svanderbleek/idris)/977 | TDDWI + more |
| 0 | 0 | 0 | Unknown | [idris-learning-2](https://github.com/jinjor/idris-learning-2)/978 | Just learning Idris |
| 0 | 0 | 0 | Unknown | [IdrisVKAPI](https://github.com/GrandArchTemplar/IdrisVKAPI)/979 | None |
| 0 | 0 | 0 | Unknown | [IdrisPractises](https://github.com/GrandArchTemplar/IdrisPractises)/980 | None |
| 0 | 0 | 0 | Unknown | [idris_experiments](https://github.com/lehmacdj/idris_experiments)/981 | None |
| 0 | 0 | 1 | Unknown | [idris-mongo](https://github.com/machunter/idris-mongo)/982 | An unworthy mongo library for Idris |
| 0 | 0 | 0 | Unknown | [learn-you-an-idris](https://github.com/Fwerskaje/learn-you-an-idris)/983 | Some notes on Idris programming language |
| 0 | 0 | 0 | Unknown | [idris-tdd-exercises](https://github.com/ioanluca/idris-tdd-exercises)/984 | exercises from the Type-Driven-Development book by Edwin Brady |
| 0 | 0 | 0 | Unknown | [effects-lib](https://github.com/cbresendiz1/effects-lib)/985 | Testing out continuations |
| 0 | 0 | 0 | Unknown | [idream_test_dep1](https://github.com/idream-build/idream_test_dep1)/986 | Fixture used during idream integration tests, serves no other real purpose. |
| 0 | 0 | 0 | Unknown | [FPIDR](https://github.com/cekcbj/FPIDR)/987 | None |
| 0 | 0 | 0 | Unknown | [sudoku](https://github.com/beefyhalo/sudoku)/988 | Idris Sudoku |
| 0 | 0 | 0 | Unknown | [idrbook](https://github.com/alexcoplan/idrbook)/989 | Somewhere to put code written while working through "Type-Driven Development with Idris" |
| 0 | 0 | 0 | Unknown | [pamperscript](https://github.com/ebenpack/pamperscript)/990 | [WIP] - Dependently typed HTML |
| 0 | 0 | 0 | Unknown | [idris-exercises](https://github.com/adrijardi/idris-exercises)/991 | Type-Driven Development with Idris - Exercises |
| 0 | 0 | 0 | Unknown | [idris-tdd](https://github.com/aterentic/idris-tdd)/992 | Type Drive Development with Idris |
| 0 | 0 | 0 | Unknown | [idris-posix-sandbox](https://github.com/KeenS/idris-posix-sandbox)/993 | None |
| 0 | 0 | 0 | Unknown | [finite-sets](https://github.com/andrevidela/finite-sets)/994 | None |
| 0 | 0 | 0 | Unknown | [crosses-zeros](https://github.com/andreykl/crosses-zeros)/995 | console game of crosses-zeros (a tic-tac-toe game) in Idris |
| 0 | 0 | 0 | Unknown | [idris_playground](https://github.com/euler2718/idris_playground)/996 | just toying around with idris |
| 0 | 0 | 0 | Unknown | [digirc](https://github.com/vikfret/digirc)/997 | [Nim/Idris] A little IRC bot, just for fun. |
| 0 | 0 | 0 | Unknown | [idris-learning](https://github.com/NefedovDA/idris-learning)/998 | None |
| 0 | 0 | 0 | Unknown | [Temp](https://github.com/andylokandy/Temp)/999 | None |
| 0 | 0 | 0 | Unknown | [idris-playground](https://github.com/simpadjo/idris-playground)/1000 | None |