on ea6bb9a help sign in
Idris-dev/src/Idris
24 files
../ AbsSyntax.hsTweak linearity checker to deal with overloaded names properly AbsSyntaxTree.hsMerge branch 'ImprovedReflection' of https://github.com/JanBessai/Idris-dev into JanBessai-ImprovedReflection Compiler.hsmake TT aware of Set -> Type Completion.hsFull TT reflection and reification 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.hsFix some INTERNAL ERRORs which aren't (non-function type, nothing to introduce) (And the crowd goes wild) Docs.hsbetter lookup for operators ElabDecls.hsTweak linearity checker to deal with overloaded names properly ElabTerm.hsMerge branch 'ImprovedReflection' of https://github.com/JanBessai/Idris-dev into JanBessai-ImprovedReflection Error.hsReorder the monad transformers in the Idris monad to allow completion Help.hsadd command to change current directory IBC.hsIBC Version number bump Imports.hsAdding support for Windows MingW32 Parser.hsFull TT reflection and reification Primitives.hsadded forgotten LStrLen primitive and length function for String Prover.hsFix error with linearity checking in patterns Providers.hsExecute type providers while typechecking REPL.hsadd command to change current directory REPLParser.hsadd command to change current directory Transforms.hsuppercase modulenames Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsReorder the monad transformers in the Idris monad to allow completion