git.iko.soy/Idris-dev
on 62be419 help sign in
Idris-dev/src/Idris
24 files
../ AbsSyntax.hsTweak linearity checker to deal with overloaded names properly AbsSyntaxTree.hsUse just-built dynamic RTS during library typecheck Compiler.hsmake TT aware of Set -> Type Completion.hsreduce duplication by providing a show instance for CmdArg Coverage.hsFix comedy error in termination checker 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.hsArguments under type constructors are not forceable! Delaborate.hsAdd type provider errors + test case Docs.hsbetter lookup for operators ElabDecls.hsAdd type provider errors + test case ElabTerm.hsIf the goal is not a function type when elaborating \, invent one ...and attempt to solve it by unification Error.hsReorder the monad transformers in the Idris monad to allow completion Help.hsadd command to change current directory IBC.hsMerge remote-tracking branch 'upstream/master' into providers Imports.hsAdding support for Windows MingW32 Parser.hsRemove type class argument restriction in parser Primitives.hsadded forgotten LStrLen primitive and length function for String Prover.hsFix error with linearity checking in patterns Providers.hsUpdate type providers so that the decision of failure or otherwise is made in IO REPL.hsUse just-built dynamic RTS during library typecheck REPLParser.hsadd command to change current directory Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsReorder the monad transformers in the Idris monad to allow completion