git.iko.soy/Idris-dev
on 0abbd53 help sign in
Idris-dev/src/Idris
25 files
../ AbsSyntax.hsinitial ideslave AbsSyntaxTree.hsuse process in ideslave loop Compiler.hsmake TT aware of Set -> Type Completion.hsFull TT reflection and reification Coverage.hsLook through call graph for mutual recursion when productivity checking Otherwise we might miss non-productive calls, particularly important when using 'with'. Fixes issue #183 DSL.hsChange meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces. DataOpts.hsRemove the unused arg from lookup functions Delaborate.hsFix :t for metavariables Fixes issue #280 Docs.hsRemove the unused arg from lookup functions ElabDecls.hsCache missing cases found by totality checker, for display Now :missing works correctly (fixes issue #210) Also, remove a large chunk of unused code in coverage checker. ElabTerm.hsDon't allow unification problems to be introduced in :p mode Error.hsReorder the monad transformers in the Idris monad to allow completion Help.hsadd command to change current directory IBC.hsEnable alternate names for shared libraries IdeSlave.hsrename abort -> error, emacs-rex -> idris Imports.hsAdding support for Windows MingW32 Parser.hsMerge branch 'MixingImplicitArgs' of https://github.com/JanBessai/Idris-dev into JanBessai-MixingImplicitArgs Primitives.hsRevert "Merge pull request #294 from bitlisp/unified-int-primitives" Prover.hsRemove the unused arg from lookup functions Providers.hsUpdate type providers so that the decision of failure or otherwise is made in IO REPL.hsrename abort -> error, emacs-rex -> idris REPLParser.hssquash potential space leaks by using strict foldl Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsRemove the unused arg from lookup functions