on 1b71663 help sign in
all commits
3ccb494Remove the empty property 'copyright'.Jan de Muijnck-Hughes 4a3fe0cLinearTypes extension improvementsEdwin Brady 83bb62fUnused binds (#4067)Jason Felice d4bd8e6Clean up unused imports (#4065)Jason Felice 5d7388bMove extensions into source filesEdwin Brady a89330eChange meaning of 'data' in interfacesEdwin Brady 6dffcc7Fix reporting of infinite unificationEdwin Brady fb185aaCheck for linearity of constructorsEdwin Brady a5033e7Add linear LamEdwin Brady e1c210bAdd 'RigCount' to Pi and PVarEdwin Brady e3daf28Add RigCount to environmentEdwin Brady e6ceb5cAlphabetize and indent imports and LANGUAGE pragmasEcho Nolan 0df1270Change Instance to implementation (#3404)(λ _ λ) 06d9db6Use interface instead class or type class in documentations (#3379)(λ _ λ) fdfa04cStore file with constraints + exportEdwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes 536372fRename Lazy' => DelayedEdwin Brady 9297ae4Allow 'data' declarations in interfacesEdwin Brady 4a4548eNormalise less when unifyingEdwin Brady 83f0af1Display expected type of RHS in error messagesEdwin Brady c931effProof search improvementsEdwin Brady b1ce3cbImplement a form of pattern unificationEdwin Brady 4932d1cPi binders can never unify with TypeEdwin Brady 2e170bfRemove dubious matching ruleEdwin Brady 8173932Improve disambiguation a bit moreEdwin Brady 3034fb6Remove argument ordering hack in elaboratorEdwin Brady f987aecAdd info field to AppEdwin Brady 13a36a3Annotate functions as %hint for auto searchEdwin Brady c66df51Propagate unification solutions into types on 'P'Edwin Brady 426d052Add provenance flag to unification errorsEdwin Brady 26cfbe9Scoped implicits fixEdwin Brady f6bcfb6Some tidying of scoped implicitsEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady 85cf83fAllow building with base-4.8.0.0RyanGlScott 713776cCheck for cycles in unification resultsEdwin Brady f01c1a1Efficiency of unificationEdwin Brady 6b6aae0Avoid retrying unification problems constantlyEdwin Brady 2905dbcLifted TODO/FIXME in Core/UnifyJan de Muijnck-Hughes 37b11f8Unification fix for chains of solutionsEdwin Brady 971d88dAnnotate several top-level functionsMichael Maloney 7e7368dStore kind in Pi bindersEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady e6e1ad9Unification fixEdwin Brady 25de16dDisjoint constants should be fatal in unificationEdwin Brady 8ed343bRemove dodgy unification hackEdwin Brady 5ffef89Type class resolution fixEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 2a0056aNew matching rule for solving simple functionsEdwin Brady