git.iko.soy/Idris-dev
on 8bbd1b5 help sign in
Idris-dev/src/Idris
23 files
../ AbsSyntax.hsFix error with linearity checking in patterns AbsSyntaxTree.hsAdded first steps in type providers Compiler.hsmake TT aware of Set -> Type Completion.hsStop completion of names that are prefixes of others 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 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.hsReformat existing comments for Haddock and add Haddock comments 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