git.iko.soy/Idris-dev
on 3dd89eb help sign in
Idris-dev/src/Idris
21 files
../ AbsSyntax.hsmake TT aware of Set -> Type AbsSyntaxTree.hsDistinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon! Compiler.hsmake TT aware of Set -> Type Coverage.hsDistinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon! 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.hsMake unification faster by computing HNF rather than normalising Docs.hsbetter lookup for operators ElabDecls.hsMore sane scoping rules for where/type classes Parameters in the type signature get propagated, indices do not. So you no longer need to pass parameters explicitly if you need them in a where clause, and you no longer need to give explicitly typed helpers … ElabTerm.hsDistinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon! Error.hsAllow inference of Sets at REPL IBC.hsDistinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon! Imports.hsAdding support for Windows MingW32 Parser.hsParse case options as patterns, not expressions Fixes issue #147 Primitives.hsadded LChInt LIntCh to primitives Prover.hsA couple of small improvements to termination checking * inlining to help out * %assert_total doesn't allow inlining so as not to break totality for functions which rely on the asserted function * bug fix for mutual recursion - build size graphs before d… REPL.hsDistinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon! REPLParser.hsMerge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascript Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsMerge branch 'master' of https://github.com/raichoo/Idris-dev