on 54e4e41 help sign in
all commits
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