git.iko.soy/Idris-dev
on aeb032a help sign in
history oftest/meta002/expected
all commits
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