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/Monad/*.idr
104 libs/base/Data/Vect/*.idr
105 libs/base/Debug/*.idr
106 libs/base/Language/Reflection/*.idr
108 libs/base/System/*.idr
109 libs/base/System/Concurrency/*.idr
110 libs/base/Syntax/*.idr
112 libs/contrib/contrib.ipkg
113 libs/contrib/Makefile
114 libs/contrib/Classes/*.idr
115 libs/contrib/Control/*.idr
116 libs/contrib/Control/Isomorphism/*.idr
117 libs/contrib/Control/Algebra/*.idr
118 libs/contrib/Data/*.idr
119 libs/contrib/Data/Nat/*.idr
120 libs/contrib/Data/Nat/DivMod/*.idr
121 libs/contrib/Decidable/*.idr
122 libs/contrib/Network/*.idr
123 libs/contrib/System/Concurrency/*.idr
125 libs/effects/Makefile
126 libs/effects/effects.ipkg
127 libs/effects/Effect/*.idr
277 test/reg051-disabled/run
278 test/reg051-disabled/*.idr
279 test/reg051-disabled/expected
328 test/basic001/expected
331 test/basic002/expected
334 test/basic003/expected
337 test/basic004/expected
340 test/basic005/expected
343 test/basic006/expected
346 test/basic007/expected
349 test/basic008/expected
352 test/basic009/expected
353 test/basic009/B/*.idr
356 test/basic010/expected
359 test/basic011/expected
362 test/basic012/expected
365 test/basic013/expected
369 test/bignum001/expected
372 test/bignum002/expected
374 test/classes001/*.idr
376 test/classes001/expected
377 test/classes001/input
379 test/corecords001/*.idr
380 test/corecords001/run
381 test/corecords001/expected
382 test/corecords002/*.idr
383 test/corecords002/run
384 test/corecords002/expected
388 test/delab001/expected
392 test/disambig001/*.idr
393 test/disambig001/expected
395 test/disambig002/*.idr
396 test/disambig002/expected
413 test/effects001/*.idr
414 test/effects001/expected
415 test/effects001/testFile
417 test/effects002/*.idr
418 test/effects002/expected
420 test/effects003/*.idr
421 test/effects003/expected
422 test/effects003/input
424 test/effects004/*.idr
425 test/effects004/expected
426 test/effects004/input
430 test/error001/expected
433 test/error002/expected
436 test/error003/expected
439 test/error004/expected
442 test/error005/expected
457 test/ffi004/theOtherType
467 test/folding001/*.idr
469 test/folding001/expected
472 test/idrisdoc001/expected
473 test/idrisdoc001/*.idr
474 test/idrisdoc001/*.ipkg
476 test/idrisdoc002/expected
477 test/idrisdoc002/*.idr
478 test/idrisdoc002/*.ipkg
480 test/idrisdoc003/expected
481 test/idrisdoc003/*.idr
482 test/idrisdoc003/*.ipkg
484 test/idrisdoc004/expected
485 test/idrisdoc004/*.idr
486 test/idrisdoc004/*.ipkg
488 test/idrisdoc005/expected
489 test/idrisdoc005/*.idr
490 test/idrisdoc005/*.ipkg
492 test/idrisdoc006/expected
493 test/idrisdoc006/A/fully/Qualified/NAME.idr
494 test/idrisdoc006/*.idr
495 test/idrisdoc006/*.ipkg
497 test/idrisdoc007/expected
498 test/idrisdoc007/*.idr
499 test/idrisdoc007/*.ipkg
501 test/idrisdoc008/expected
502 test/idrisdoc008/*.idr
503 test/idrisdoc008/*.ipkg
505 test/idrisdoc009/expected
506 test/idrisdoc009/input
507 test/idrisdoc009/*.idr
510 test/interactive001/run
511 test/interactive001/input
512 test/interactive001/*.idr
513 test/interactive001/expected
514 test/interactive002/run
515 test/interactive002/input
516 test/interactive002/*.idr
517 test/interactive002/expected
518 test/interactive003/run
519 test/interactive003/input
520 test/interactive003/*.idr
521 test/interactive003/expected
522 test/interactive004/run
523 test/interactive004/input
524 test/interactive004/*.idr
525 test/interactive004/expected
526 test/interactive005/run
527 test/interactive005/input
528 test/interactive005/*.idr
529 test/interactive005/expected
530 test/interactive006/run
531 test/interactive006/input
532 test/interactive006/*.idr
533 test/interactive006/expected
534 test/interactive007/run
535 test/interactive007/input
536 test/interactive007/expected
537 test/interactive008/run
538 test/interactive008/input
539 test/interactive008/expected
552 test/literate001/*.lidr
553 test/literate001/expected
557 test/meta001/expected
560 test/meta002/expected
562 test/primitives001/run
563 test/primitives001/*.idr
564 test/primitives001/expected
565 test/primitives002/run
566 test/primitives002/expected
567 test/primitives003/run
568 test/primitives003/*.idr
569 test/primitives003/expected
573 test/proof001/expected
576 test/proof002/expected
579 test/proof003/expected
582 test/proof004/expected
585 test/proof005/expected
588 test/proof006/expected
591 test/proof007/expected
594 test/proof008/expected
597 test/proof009/expected
601 test/proof010/expected
603 test/quasiquote001/run
604 test/quasiquote001/*.idr
605 test/quasiquote001/expected
606 test/quasiquote002/run
607 test/quasiquote002/*.idr
608 test/quasiquote002/expected
609 test/quasiquote003/run
610 test/quasiquote003/*.idr
611 test/quasiquote003/expected
612 test/quasiquote004/run
613 test/quasiquote004/*.idr
614 test/quasiquote004/expected
615 test/quasiquote005/run
616 test/quasiquote005/*.idr
617 test/quasiquote005/expected
618 test/quasiquote006/run
619 test/quasiquote006/*.idr
620 test/quasiquote006/expected
623 test/records001/*.idr
624 test/records001/expected
626 test/records002/*.idr
627 test/records002/expected
629 test/records003/*.idr
630 test/records003/expected
632 test/sourceLocation001/run
633 test/sourceLocation001/*.idr
634 test/sourceLocation001/expected
638 test/sugar001/expected
641 test/sugar002/expected
644 test/sugar003/expected
647 test/sugar004/expected
650 test/sugar005/expected
654 test/syntax001/expected
657 test/tactics001/*.idr
658 test/tactics001/expected
661 test/totality001/*.idr
662 test/totality001/expected
664 test/totality002/*.idr
665 test/totality002/expected
667 test/totality003/*.idr
668 test/totality003/expected
670 test/totality004/*.idr
671 test/totality004/expected
673 test/totality005/*.idr
674 test/totality005/expected
676 test/totality006/*.idr
677 test/totality006/expected
679 test/totality007/*.ipkg
680 test/totality007/src/*.idr
681 test/totality007/expected
683 test/totality008/*.idr
684 test/totality008/expected
686 test/totality009/*.idr
687 test/totality009/expected
690 test/tutorial001/*.idr
691 test/tutorial001/expected
693 test/tutorial002/*.idr
694 test/tutorial002/expected
696 test/tutorial003/*.idr
697 test/tutorial003/expected
699 test/tutorial004/*.idr
700 test/tutorial004/expected
702 test/tutorial005/*.idr
703 test/tutorial005/expected
705 test/tutorial006/*.idr
706 test/tutorial006/expected
710 test/unique001/expected
713 test/unique002/expected
716 test/unique003/expected
721 test/docs001/expected
725 test/docs002/expected
729 test/docs003/expected
732source-repository head
734 location: git://github.com/idris-lang/Idris-dev.git
737 Description: Build support for libffi
742 Description: Use GMP for Integers
747 Description: Use Curses to get the screen width
751-- This flag determines whether to show Git hashes in version strings
752-- Defaults to True because Hackage is a source release
754 Description: This is an official release
759 Description: Build an Idris that doesn't use cabal
764 Description: Built everything using "-Werror", meant for CI-builds only
769 Description: Build executables only, skip the libraries and RTS
777 , Idris.Core.CaseTree
778 , Idris.Core.Constraints
780 , Idris.Core.Elaborate
781 , Idris.Core.Evaluate
783 , Idris.Core.ProofState
784 , Idris.Core.ProofTerm
786 , Idris.Core.Typecheck
797 , Idris.Elab.Instance
798 , Idris.Elab.Provider
799 , Idris.Elab.Transform
806 , Idris.AbsSyntaxTree
822 , Idris.ElabQuasiquote
857 , IRTS.CodegenJavaScript
859 , IRTS.JavaScript.AST
861 , IRTS.Defunctionalise
885 Build-depends: base >=4 && <5
886 , annotated-wl-pprint >= 0.5.3 && < 0.7
887 , ansi-terminal < 0.7
888 , ansi-wl-pprint < 0.7
889 , base64-bytestring < 1.1
890 , binary >= 0.7 && < 0.8
891 , blaze-html >= 0.6.1.3 && < 0.9
892 , blaze-markup >= 0.5.2.1 && < 0.8
895 , containers >= 0.5 && < 0.6
897 , directory >= 1.2.2.0 && < 1.3
899 , fingertree >= 0.1 && < 0.2
900 , haskeline >= 0.7 && < 0.8
901 , lens >= 4.1.1 && < 4.12
902 , mtl >= 2.1 && < 2.3
904 , optparse-applicative >= 0.11 && < 0.12
905 , parsers >= 0.9 && < 0.13
909 , text >=1.2.1.0 && < 1.3
910 , time >= 1.4 && < 1.6
912 , transformers-compat >= 0.3
913 , trifecta >= 1.1 && < 1.6
914 , uniplate >=1.6 && < 1.7
915 , unordered-containers < 0.3
918 , vector-binary-instances < 0.3
919 , zip-archive > 0.2.3.5 && < 0.2.4
922 Extensions: MultiParamTypeClasses
925 , FunctionalDependencies
930 ghc-prof-options: -auto-all -caf-all
931 ghc-options: -threaded -rtsopts
935 build-depends: unix < 2.8
937 cpp-options: -DFREEBSD
938 build-depends: unix < 2.8
940 cpp-options: -DDRAGONFLY
941 build-depends: unix < 2.8
943 cpp-options: -DMACOSX
944 build-depends: unix < 2.8
946 cpp-options: -DWINDOWS
947 build-depends: Win32 < 2.4
949 build-depends: libffi < 0.2
950 cpp-options: -DIDRIS_FFI
952 build-depends: libffi < 0.2
953 cpp-options: -DIDRIS_GMP
955 build-depends: hscurses < 1.5
956 cpp-options: -DCURSES
957 if flag(freestanding)
958 other-modules: Target_idris
959 cpp-options: -DFREESTANDING
974 ghc-prof-options: -auto-all -caf-all
975 ghc-options: -threaded -rtsopts -funbox-strict-fields
979 hs-source-dirs: codegen/idris-c
987 ghc-prof-options: -auto-all -caf-all
988 ghc-options: -threaded -rtsopts -funbox-strict-fields
990Executable idris-javascript
992 hs-source-dirs: codegen/idris-javascript
1000 ghc-prof-options: -auto-all -caf-all
1001 ghc-options: -threaded -rtsopts -funbox-strict-fields
1003Executable idris-node
1005 hs-source-dirs: codegen/idris-node
1007 Build-depends: idris
1013 ghc-prof-options: -auto-all -caf-all
1014 ghc-options: -threaded -rtsopts -funbox-strict-fields
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