git.iko.soy/Idris-dev
on ab89bf0 help sign in
Idris-dev/src/Idris
24 files
../ AbsSyntax.hsFix error with linearity checking in patterns AbsSyntaxTree.hsAdded first steps in type providers Compiler.hsmake TT aware of Set -> Type Completion.hsunify help and completion of REPL - previously they were not in sync, now it is one lookup table 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.hsAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution! Docs.hsbetter lookup for operators ElabDecls.hsAdded first steps in type providers ElabTerm.hsFix error with linearity checking in patterns Error.hsReorder the monad transformers in the Idris monad to allow completion Help.hsunify help and completion of REPL - previously they were not in sync, now it is one lookup table IBC.hsAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution! Imports.hsAdding support for Windows MingW32 Parser.hsAdded first steps in type providers Primitives.hsMerge branch 'master' of git://github.com/edwinb/Idris-dev into bitstring Prover.hsFix error with linearity checking in patterns Providers.hsAdded first steps in type providers REPL.hsunify help and completion of REPL - previously they were not in sync, now it is one lookup table REPLParser.hsjavascript: split javascript and node target Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsReorder the monad transformers in the Idris monad to allow completion