on 1b71663 help sign in
all commits
3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 4a3fe0cLinearTypes extension improvementsEdwin Brady 7e800caSmall tweak to inliningEdwin Brady 83bb62fUnused binds (#4067)Jason Felice 5950e1ePrevent private functions showing up in autocomplete and :t.Steven Shaw ffd2db0Fix for evaluation of partial things at the REPLEdwin Brady 4a6974cFix ordering of patterns in conversion checkEdwin Brady 6dffcc7Fix reporting of infinite unificationEdwin Brady a1e3b5bRevert to normalising from WHNFEdwin Brady 0ceaa30Deal with interfaces in totality differentlyEdwin Brady b30e112add a type alias for the TT Declaration as it is getting unwieldyjoe9 9e69858Fixed unstylized things in Idris and stylize.sh scriptAhmad Salim Al-Sibahi ad13438Check linear types in binders are validEdwin Brady 89dd6aeCheck linearity of functionsEdwin Brady a5033e7Add linear LamEdwin Brady 1e3651fCheck multiplicities on RigCountsEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady 4c4a07aChange evaluation of partial functions at REPLEdwin Brady ea88b5eBetter choice of pattern to inspect in coverageEdwin Brady b28f12bWHNF takes an environmentEdwin Brady 521b8bfRemove unused case tree codeEdwin Brady 7537cc4Change totality checking and inliningEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 9c636f4Remove a bunch of "deriving instance NFData" hot commentsEcho Nolan f754d9cPurify Idris of "return"David Christiansen 02d29f5Fix conversion of case blocksEdwin Brady 45bf2b6Fix ordering of run time case treesEdwin Brady 9baa5ceUse GHC generics for NFData instancesEcho Nolan 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes d6a185aReduction limit when simplifyingEdwin Brady b03f823Fix evaluation of InfEdwin Brady fdfa04cStore file with constraints + exportEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes 9297ae4Allow 'data' declarations in interfacesEdwin Brady fe1d470Totality checking now looks inside case directlyEdwin Brady 8df6b32prim__believeMe needs to be considered totalEdwin Brady faa58adFix evaluation of non-total thingsEdwin Brady 2392716Fix silly error in totality checkerEdwin Brady 6c682f3Comment editingEdwin Brady fdfd99eFix behaviour of %hideEdwin Brady e3e35a5New rules for name visibilityEdwin Brady a14e4edSimplify export rules.Edwin Brady b1872fbFile IO type indicates possibility of failureEdwin Brady 1cdc9ddReduce space leak through ugly DeepSeq hackDavid Raymond Christiansen a24c7d4Finish WHNF for operatorsEdwin Brady 64df5f6Added WHNF moduleEdwin Brady 7f20febDon't totality check PE definitionsEdwin Brady 4dabdbaPropagate errors originating from case treesDavid Raymond Christiansen 5b73dcbFix the broken 'Exact' versions of lookupsEdwin Brady