git.iko.soy/Idris-dev
on df5bf81 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.hsReformat existing comments for Haddock and add Haddock comments 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 '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.hsNormalise before looking for coercions 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.hsMissing case in Idris.Parser Primitives.hsMerge branch 'master' of git://github.com/edwinb/Idris-dev into bitstring Prover.hsCheck the type of a proof matches the type of the goal! 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