6Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
7Homepage: http://www.idris-lang.org/
10Category: Compilers/Interpreters, Dependent Types
11Synopsis: Functional Programming Language with Dependent Types
12Description: Idris is a general purpose language with full dependent types.
13 It is compiled, with eager evaluation.
14 Dependent types allow types to be predicated on values,
15 meaning that some aspects of a program's behaviour can be
16 specified precisely in the type. The language is closely
17 related to Epigram and Agda. There is a tutorial at
18 <http://www.idris-lang.org/documentation>.
21 * Full dependent types with dependent pattern matching
23 * where clauses, with rule, simple case expressions,
24 pattern matching let and lambda bindings
26 * Type classes, monad comprehensions
28 * do notation, idiom brackets, syntactic conveniences for lists,
29 tuples, dependent pairs
35 * Indentation significant syntax, extensible syntax
37 * Tactic based theorem proving (influenced by Coq)
39 * Cumulative universes
41 * Simple foreign function interface (to C)
43 * Hugs style interactive environment
49Data-files: idrisdoc/styles.css
50 jsrts/Runtime-browser.js
51 jsrts/Runtime-common.js
55 rts/arduino/idris_main.c
91 libs/prelude/prelude.ipkg
92 libs/prelude/Prelude/*.idr
93 libs/prelude/Decidable/*.idr
94 libs/prelude/Language/*.idr
95 libs/prelude/Language/Reflection/*.idr
101 libs/base/Control/*.idr
102 libs/base/Control/Isomorphism/*.idr
103 libs/base/Control/Monad/*.idr
105 libs/base/Data/Vect/*.idr
106 libs/base/Debug/*.idr
107 libs/base/Decidable/*.idr
108 libs/base/Language/Reflection/*.idr
110 libs/base/Network/*.idr
111 libs/base/System/*.idr
112 libs/base/System/Concurrency/*.idr
113 libs/base/Syntax/*.idr
116 libs/effects/Makefile
117 libs/effects/effects.ipkg
118 libs/effects/Effect/*.idr
292 test/basic001/expected
295 test/basic002/expected
298 test/basic003/expected
301 test/basic004/expected
304 test/basic005/expected
307 test/basic006/expected
310 test/basic007/expected
313 test/basic008/expected
316 test/basic009/expected
317 test/basic009/B/*.idr
320 test/basic010/expected
323 test/basic011/expected
326 test/basic012/expected
328 test/buffer001-disabled/*.idr
329 test/buffer001-disabled/run
330 test/buffer001-disabled/expected
334 test/delab001/expected
349 test/effects001/*.idr
350 test/effects001/expected
351 test/effects001/testFile
353 test/effects002/*.idr
354 test/effects002/expected
356 test/effects003/*.idr
357 test/effects003/expected
358 test/effects003/input
362 test/error001/expected
365 test/error002/expected
368 test/error003/expected
371 test/error004/expected
374 test/error005/expected
389 test/ffi004/theOtherType
396 test/idrisdoc001/expected
397 test/idrisdoc001/*.idr
398 test/idrisdoc001/*.ipkg
400 test/idrisdoc002/expected
401 test/idrisdoc002/*.idr
402 test/idrisdoc002/*.ipkg
404 test/idrisdoc003/expected
405 test/idrisdoc003/*.idr
406 test/idrisdoc003/*.ipkg
408 test/idrisdoc004/expected
409 test/idrisdoc004/*.idr
410 test/idrisdoc004/*.ipkg
412 test/idrisdoc005/expected
413 test/idrisdoc005/*.idr
414 test/idrisdoc005/*.ipkg
416 test/idrisdoc006/expected
417 test/idrisdoc006/A/fully/Qualified/NAME.idr
418 test/idrisdoc006/*.idr
419 test/idrisdoc006/*.ipkg
421 test/idrisdoc007/expected
422 test/idrisdoc007/*.idr
423 test/idrisdoc007/*.ipkg
425 test/idrisdoc008/expected
426 test/idrisdoc008/*.idr
427 test/idrisdoc008/*.ipkg
429 test/idrisdoc009/expected
430 test/idrisdoc009/input
431 test/idrisdoc009/*.idr
434 test/interactive001/run
435 test/interactive001/input
436 test/interactive001/*.idr
437 test/interactive001/expected
438 test/interactive002/run
439 test/interactive002/input
440 test/interactive002/*.idr
441 test/interactive002/expected
442 test/interactive003/run
443 test/interactive003/input
444 test/interactive003/*.idr
445 test/interactive003/expected
446 test/interactive004/run
447 test/interactive004/input
448 test/interactive004/*.idr
449 test/interactive004/expected
450 test/interactive005/run
451 test/interactive005/input
452 test/interactive005/*.idr
453 test/interactive005/expected
454 test/interactive006/run
455 test/interactive006/input
456 test/interactive006/*.idr
457 test/interactive006/expected
470 test/literate001/*.lidr
471 test/literate001/expected
473 test/primitives001/run
474 test/primitives001/*.idr
475 test/primitives001/expected
476 test/primitives002/run
477 test/primitives002/expected
478 test/primitives003/run
479 test/primitives003/*.idr
480 test/primitives003/expected
484 test/proof001/expected
487 test/proof002/expected
490 test/proof003/expected
493 test/proof004/expected
495 test/quasiquote001/run
496 test/quasiquote001/*.idr
497 test/quasiquote001/expected
498 test/quasiquote002/run
499 test/quasiquote002/*.idr
500 test/quasiquote002/expected
501 test/quasiquote003/run
502 test/quasiquote003/*.idr
503 test/quasiquote003/expected
504 test/quasiquote004/run
505 test/quasiquote004/*.idr
506 test/quasiquote004/expected
510 test/records001/*.idr
511 test/records001/expected
513 test/records002/*.idr
514 test/records002/expected
516 test/records003/*.idr
517 test/records003/expected
519 test/sourceLocation001/run
520 test/sourceLocation001/*.idr
521 test/sourceLocation001/expected
525 test/sugar001/expected
528 test/sugar002/expected
531 test/sugar003/expected
534 test/sugar004/expected
537 test/sugar005/expected
541 test/totality001/*.idr
542 test/totality001/expected
544 test/totality002/*.idr
545 test/totality002/expected
547 test/totality003/*.idr
548 test/totality003/expected
550 test/totality004/*.idr
551 test/totality004/expected
553 test/totality005/*.idr
554 test/totality005/expected
556 test/totality006/*.idr
557 test/totality006/expected
559 test/totality007/*.ipkg
560 test/totality007/src/*.idr
561 test/totality007/expected
563 test/totality008/*.idr
564 test/totality008/expected
567 test/tutorial001/*.idr
568 test/tutorial001/expected
570 test/tutorial002/*.idr
571 test/tutorial002/expected
573 test/tutorial003/*.idr
574 test/tutorial003/expected
576 test/tutorial004/*.idr
577 test/tutorial004/expected
579 test/tutorial005/*.idr
580 test/tutorial005/expected
582 test/tutorial006/*.idr
583 test/tutorial006/expected
587 test/unique001/expected
590 test/unique002/expected
593 test/unique003/expected
595source-repository head
597 location: git://github.com/idris-lang/Idris-dev.git
600 Description: Build support for libffi
605 Description: Use GMP for Integers
610 Description: Use Curses to get the screen width
614-- This flag determines whether to show Git hashes in version strings
615-- Defaults to True because Hackage is a source release
617 Description: This is an official release
622 Description: Build an Idris that doesn't use cabal
627 Description: Built everything using "-Werror", meant for CI-builds only
635 , Idris.Core.CaseTree
636 , Idris.Core.Constraints
638 , Idris.Core.Elaborate
639 , Idris.Core.Evaluate
641 , Idris.Core.ProofState
642 , Idris.Core.ProofTerm
644 , Idris.Core.Typecheck
654 , Idris.Elab.Instance
655 , Idris.Elab.Provider
656 , Idris.Elab.Transform
660 , Idris.AbsSyntaxTree
675 , Idris.ElabQuasiquote
710 , IRTS.CodegenJavaScript
711 , IRTS.JavaScript.AST
713 , IRTS.Defunctionalise
737 Build-depends: base >=4 && <5
738 , annotated-wl-pprint >= 0.5.3 && < 0.6
739 , ansi-terminal < 0.7
740 , ansi-wl-pprint < 0.7
741 , base64-bytestring < 1.1
742 , binary >= 0.7 && < 0.8
743 , blaze-html >= 0.6.1.3 && < 0.8
744 , blaze-markup >= 0.5.2.1 && < 0.7.0.0
747 , containers >= 0.5 && < 0.6
749 , directory >= 1.2 && < 1.3
751 , fingertree >= 0.1 && < 0.2
752 , haskeline >= 0.7 && < 0.8
753 , lens >= 4.1.1 && < 4.8
754 , mtl >= 2.2.1 && < 2.3
756 , optparse-applicative >= 0.11 && < 0.12
757 , parsers >= 0.9 && < 0.13
762 , time >= 1.4 && < 1.6
764 , trifecta >= 1.1 && < 1.6
765 , uniplate >=1.6 && < 1.7
766 , unordered-containers < 0.3
769 , vector-binary-instances < 0.3
772 Extensions: MultiParamTypeClasses
775 , FunctionalDependencies
780 ghc-prof-options: -auto-all -caf-all
781 ghc-options: -threaded -rtsopts
785 build-depends: unix < 2.8
787 cpp-options: -DFREEBSD
788 build-depends: unix < 2.8
790 cpp-options: -DDRAGONFLY
791 build-depends: unix < 2.8
793 cpp-options: -DMACOSX
794 build-depends: unix < 2.8
796 cpp-options: -DWINDOWS
797 build-depends: Win32 < 2.4
799 build-depends: libffi < 0.2
800 cpp-options: -DIDRIS_FFI
802 build-depends: libffi < 0.2
803 cpp-options: -DIDRIS_GMP
805 build-depends: hscurses < 1.5
806 cpp-options: -DCURSES
807 if flag(freestanding)
808 other-modules: Target_idris
809 cpp-options: -DFREESTANDING
824 ghc-prof-options: -auto-all -caf-all
825 ghc-options: -threaded -rtsopts -funbox-strict-fields
829 hs-source-dirs: codegen/idris-c
837 ghc-prof-options: -auto-all -caf-all
838 ghc-options: -threaded -rtsopts -funbox-strict-fields
840Executable idris-javascript
842 hs-source-dirs: codegen/idris-javascript
850 ghc-prof-options: -auto-all -caf-all
851 ghc-options: -threaded -rtsopts -funbox-strict-fields -O2
855 hs-source-dirs: codegen/idris-node
863 ghc-prof-options: -auto-all -caf-all
864 ghc-options: -threaded -rtsopts -funbox-strict-fields -O2
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list