git.iko.soy/Idris-dev
on ca34dec help sign in
history oftest/meta002/expected
all commits
f743272Don't include '=' for RHS spanJason Felice 79351eeAdd blank line after "large" messagesJason Felice 7d0c06bPut source code before error (like parse errors)Jason Felice f967817Make warnings, non-parse errors prettyJason Felice b1a4264Improve error message locations (#4210)Jason Felice 58c3bb7Hide more features behind %language pragmasEdwin Brady 8d78d32Add some Quotable implementations (#3104)Melvar Chen 0f00278Generalize the types of mkApp and unApplyDavid Christiansen eaf5211Add the ability to define datatypes in ElabDavid Raymond Christiansen fd2501bRenamed `DepPair` to DPairJan de Muijnck-Hughes ed2bda5Updates to renaming dependent pairs.Jan de Muijnck-Hughes 04f1d91Update Agda-style reflection test with quoteGoalDavid Raymond Christiansen 83f0af1Display expected type of RHS in error messagesEdwin Brady f7e1990Add lookup of FunArgs for global names to ElabDavid Raymond Christiansen 5330e8aSimplifications to ElabDavid Raymond Christiansen 83aa146Stop let-binding Elab scripts around their holesDavid Raymond Christiansen 76bcaf2Add the ability to look up if a name is a TC to ElabDavid Raymond Christiansen 071d34bMake name operations on PTerm quotation-awareDavid Raymond Christiansen ff60396Make apply match internal behaviourDavid Raymond Christiansen 85a9d50Update error messages in testsEdwin Brady 28e2668Add reasonable tests for elaborator reflectionDavid Raymond Christiansen