on d3fa352 help sign in
all commits
0ceaa30Deal with interfaces in totality differentlyEdwin Brady 3ab7affAdd Eq instance for RawDavid Christiansen 0df1270Change Instance to implementation (#3404)(λ _ λ) 8442cefDeprecate '%assert_total'Edwin Brady fc3e88cMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady fdfa04cStore file with constraints + exportEdwin Brady be093dcAdded more context to the no rewriting error, to include terms being rewritten withAhmad Salim Al-Sibahi 0f00278Generalize the types of mkApp and unApplyDavid Christiansen 1cf8fe9Context for "Can't find implementation"Edwin Brady c2d79d7Merge pull request #2930 from david-christiansen/syntax-quote-refNiklas Larsson 1639d15Fix missing cases in Show for ConstDavid Raymond Christiansen 68c019aChange export qualifier keywordsEdwin Brady a14e4edSimplify export rules.Edwin Brady 4d0a065Change "class/instance" keywordsEdwin Brady fe3b1a3Merge remote-tracking branch 'upstream/master' into shlevy-elab-lookup-function-defDavid Raymond Christiansen 0a6313dReplace private Show FunClause with public oneMelvar Chen 42eeb6eUpdate reflection for Float -> Double changeDavid Raymond Christiansen 5330e8aSimplifications to ElabDavid Raymond Christiansen 0f89577Remove NErasedDavid Raymond Christiansen d5b66a9Show source location of case block namesDavid Raymond Christiansen b774d12Remove NLet binder from reflection APIDavid Raymond Christiansen 105c230Simplify reflection and RawDavid Raymond Christiansen cf6c277Add Eq instance for Universe in reflectionDavid Raymond Christiansen 603b06cAdd missing Show instance for CtorArgDavid Raymond Christiansen 3b90559Indicate constructor fields vs parameters in ElabDavid Raymond Christiansen e1c79efBetter error when no alternative is validEdwin Brady aee82eeFix up a couple Show instances I missed when convertingMelvar Chen 124074aAdd erasure info to Elab reflectionDavid Raymond Christiansen 1fec4faAdd showPrec to ShowMelvar Chen 1054d7dAdd UnknownImplicit errorEdwin Brady 9917c9eAdd more ShowDavid Raymond Christiansen e81efdbFix a few reflection helpersDavid Raymond Christiansen 86d1510Idiom brackets for Raw termsDavid Raymond Christiansen d6458bbAdd `{n} for quotations of the global name nDavid Raymond Christiansen 95eee3cRemove no longer used primitives from TTEdwin Brady 73ea02bRemove Buffer and BitVector from parserEdwin Brady dbe0a3cCheck class arguments for injectivityEdwin Brady c66df51Propagate unification solutions into types on 'P'Edwin Brady 348ddceError reflection for FinDavid Raymond Christiansen 0d8a153New way of dealing with unmatchable patternsEdwin Brady bcd2db1Check target of 'with' is a value (not a function)Edwin Brady 7e7368dStore kind in Pi bindersEdwin Brady a73b6afFix reference to broken primitivesDavid Raymond Christiansen 9884992Update Eq and Show reflection for internals changesDavid Raymond Christiansen 5e0a984Remove the ability to reflect At and ElaboratingDavid Raymond Christiansen b4943a2Update error reflection for CantSolveGoalDavid Raymond Christiansen 08e12c9Add Show instances for SourceLocation and ErrDavid Raymond Christiansen a338273Remove needless Prelude importsEdwin Brady 40924dcMoved libraries around, removed 'effects' flagEdwin Brady