git.iko.soy/Idris-dev
on 10ea548 help sign in
10ea548Inline type class applications where possible to reduce overheadEdwin Brady 42ca063:d to display elaborated pattern definitionEdwin Brady baaba44Run-time forcing optimisationEdwin Brady 02881b1Implemented forcing optimisation Constructor arguments which are inferrable from the indices in the constructor type are erased both at compile-time and run-timeEdwin Brady 19f1e3aCompatibility with old ghcEdwin Brady c82f2f4Add nullPtr/validFileEdwin Brady 969e573Checking elaborated term and inferred term matchEdwin Brady 3af0ae0Elaborator tweak, dealing better with values that are inferred automaticallyEdwin Brady 22b2879Making IO lazy means we need to force an evaluation for anything to happen at all...Edwin Brady 598160cMake foreign calls lazily (or they get executed at the wrong time...)Edwin Brady f3ce933Some prelude shufflingEdwin Brady 2ce525eintros tactic; some library tinkeringEdwin Brady a33b4c2Avoid adding duplicate information to .ibc => quicker load timeEdwin Brady 201ade9Fixed accessibility bug; added some library functionsEdwin Brady 0b9cab2Note on cumulativity in tutorialEdwin Brady b656c55Some mult proofsEdwin Brady 79aae2fUnification tweak - try a different order on failureEdwin Brady 7f74f91Fix error handling again in replEdwin Brady 62ea7f8Add prelude.fin moduleEdwin Brady b20f2f8Tinker with compiler interfaceEdwin Brady 264f8a6Handle Ctrl-CEdwin Brady 4ca34ffFix error recovery in replEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 628b851Added Cast to the prelude, and defined casts between primitivesEdwin Brady 8b1e498Change 'data' and where syntax so that they don't need '|' This breaks old code - instead ofEdwin Brady 2852e71Made do notation behave better when bracketedEdwin Brady c5e3aa7Debraced rest of libEdwin Brady 0b98a91Debraced tutorialEdwin Brady b0f47e1Made braces optional (at the expense of 'with' now needing the expression to be tested in brackets) do notation doesn't quite behave right - the first token after the do block must be at a lower level of indentation, which means putting it in brackets is awkward.Edwin Brady 4804676Compiler saturates constructors before compilingEdwin Brady 961d2a3FormattingEdwin Brady 24436b1No need for old-time either...Edwin Brady d13cd8eRemove unix dependencyEdwin Brady 2e9fcd4Remove semicolons in tutorialEdwin Brady ead54e4Removed semicolons from testsEdwin Brady bd61594Removed need for terminating ; A declaration is now considered terminated on encountering a token in the same column as the declaration began - or on encountering a semicolon. Libraries and some tests updated.Edwin Brady c8b0f28Use new syntax in libEdwin Brady f7c50cfMonad comprehension exampleEdwin Brady 37bb964Document comprehensionsEdwin Brady 817c1a0Monad comprehension notationEdwin Brady 93c06b5Some formattingEdwin Brady 02701e7Numeric ranges [a..b], [a,b .. c] and list monadEdwin Brady 2a50169Added lib/network directory, and network.cgi moduleEdwin Brady 38da9bcUpdate .cabal; require up to date epicEdwin Brady e24955aNote on where scoping and types in tutorialEdwin Brady 63fd5f6Documented case expressionsEdwin Brady 6196bbcAllow types on let in do blocksEdwin Brady 947c2b3Fix bug in generation of case functionsEdwin Brady a328ff1update tutorial pdfEdwin Brady e62b7eaPattern matching lambda, plus tutorial updateEdwin Brady