Skip to content
This repository

A Dependently Typed Functional Programming Language

Add :refine (:ref) command for refining a hole

Like :ps, but instead of a recursive search, it simply applies the
function given and fills in other arguments *by unification only*.

(In particular, this means it will fail if any implicit arguments need
other arguments, rather than the return type, in order to be solved by

So, this will work:

append : (n, m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a
append Z m [] ys = ys
append (S k) m (x :: xs) ys = x :: ?append_rhs1

*testref> :ref 6 append_rhs1 append
append k m ?append_rhs2 ?append_rhs3

But this will not:

vZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vZipWith f [] [] = []
vZipWith f (x :: xs) (y :: ys) = f x y :: ?vZipWith_rhs1

*Vect> :ref 18 vZipWith_rhs1 vZipWith

...because unification alone is not enough to work out the implicit
arguments a and b (even if there is only one thing that will work, it
needs a deeper proof search to find it).
latest commit e07c13d42d
Edwin Brady edwinb authored April 17, 2014
Octocat-spinner-32 benchmarks Change from shebangs with absolute references to using /usr/bin/env November 18, 2013
Octocat-spinner-32 contribs Upstream updates to idrislang.sty March 10, 2014
Octocat-spinner-32 examples Remove example directory April 10, 2014
Octocat-spinner-32 iif Change TRACE mode to use -O2 September 05, 2012
Octocat-spinner-32 jsrts javascript: initial Bits8 support April 12, 2014
Octocat-spinner-32 libs Merge pull request #1073 from david-christiansen/docs April 17, 2014
Octocat-spinner-32 llvm Fix .PHONY targets in Makefiles January 11, 2014
Octocat-spinner-32 main Make --nowarnreach the default (for now). April 11, 2014
Octocat-spinner-32 papers Fix .PHONY targets in Makefiles January 11, 2014
Octocat-spinner-32 rts Fix deadlock in RTS when using allocation in native code April 01, 2014
Octocat-spinner-32 samples New syntax for documentation comments March 03, 2014
Octocat-spinner-32 src Add :refine (:ref) command for refining a hole April 17, 2014
Octocat-spinner-32 support Fix .PHONY targets in Makefiles January 11, 2014
Octocat-spinner-32 test Add :refine (:ref) command for refining a hole April 17, 2014
Octocat-spinner-32 .gitattributes typo fix in git attributes, adding test results to gitignore November 26, 2012
Octocat-spinner-32 .gitignore Update .gitignore for new tests structure February 01, 2014
Octocat-spinner-32 .travis.yml Regression test for infinite regress in executor April 07, 2014
Octocat-spinner-32 CHANGELOG Update CHANGELOG for metavars in IDESlave April 09, 2014
Octocat-spinner-32 Updates to contributing guidelines. January 22, 2014
Octocat-spinner-32 CONTRIBUTORS Add self to contributors February 01, 2014
Octocat-spinner-32 LICENSE Fix LICENSE September 14, 2011
Octocat-spinner-32 Makefile Syntax for failures in pattern matching let/<- March 07, 2014
Octocat-spinner-32 README changed the first sentence of the readme April 01, 2014
Octocat-spinner-32 Setup.hs Add DragonFly to January 05, 2014
Octocat-spinner-32 * Use cc as C compiler, instead of hardcoding gcc. November 19, 2013
Octocat-spinner-32 Automatically detect console width February 02, 2014
Octocat-spinner-32 idris-tutorial.pdf Tutorial changes. November 28, 2013
Octocat-spinner-32 idris.cabal Add :refine (:ref) command for refining a hole April 17, 2014
Octocat-spinner-32 Update version number to 0.9.11 February 04, 2014
Idris ( is a general-purpose functional programming 
language with dependent types.

To configure, edit The default values should work for most people.

To install, type 'make'. This will install everything using cabal and
typecheck the libraries.

To run the tests, type 'make test' which will execute the test suite, and
'make relib', which will typecheck and recompile the standard library.

Idris has optional buildtime dependencies on the C libraries llvm-3.3 and libffi. If you would like to use the features that these enable, be sure these are compiled for the same architecture as your Haskell compiler (e.g. 64 bit libraries for 64 bit ghc). By default, Idris builds without them. To build with them, pass the flags -f LLVM and -f FFI, respectively.

To build with LLVM and libffi by default, create or add the following line to it:
The file is a suitable example.

Idris has a runtime dependency on libgmp, and on Boehm GC (libgc) when using the LLVM codegen. These are needed for linking into compiled programs, so be sure these are compiled for Idris's default target architecture (usually 64 bit on x86_64 systems).

The Idris wiki contains instructions for building on various platforms and for getting involved with development. It is located at .
Something went wrong with that request. Please try again.