git.iko.soy/Idris-dev
on 4187c57 help sign in
Idris-dev/src/Idris
22 files
../ AbsSyntax.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! AbsSyntaxTree.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! Compiler.hsmake TT aware of Set -> Type Completion.hsCrude support for completion in prover Coverage.hsMake coverage checker a lot faster ...with strategic use of 'nub' so as not to generate a crazy number of clauses! 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 '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! ElabTerm.hsFix error with coercions in function arguments 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 '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! Primitives.hsMerge branch 'master' of git://github.com/edwinb/Idris-dev into bitstring Prover.hsManually track prover history REPL.hsjavascript: split javascript and node target 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