git.iko.soy/Idris-dev
on aa8aefd help sign in
history ofsrc/Idris/DataOpts.hs
all commits
fb2b17dAdd collapsing optimisation and more aggressive erasureEdwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin 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