git.iko.soy/Idris-dev
on 22143e4 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
77ca4edFix interactive editing and testsDavid Raymond Christiansen 4c76d56Respect precedence and associativity for infix ops in pprintDavid Raymond Christiansen bfe6499Give the pretty-printer access to info about infixesDavid Raymond Christiansen 4035b5dAdd a field for parameter docstrings in the PClass constructor of PDecl'Paul Koerbitz af3816eMerge branch 'master' into fix/1047-repl-doc-for-typeclassesPaul Koerbitz 5a5eecaMerge pull request #1143 from ahmadsalim/bug/inductionfixDavid Christiansen d6a3eaeCareful with shadowing when abstracting withEdwin Brady 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi 6a99256Remove the REPL Info commandPaul Koerbitz 42fb8bfMerge branch 'repl'raichoo 31ca891Parse _|_ as a name in :docDavid Raymond Christiansen eea6bcbwhitespaceraichoo 51394aaAdd 'unify' tacticEdwin Brady 3badee5Merge pull request #1097 from david-christiansen/pprintEdwin Brady ee4c96eCorrect opening brace in implicits in pprinterDavid Raymond Christiansen 66a2636Docstring improvement for prop. eq.David Raymond Christiansen 5bd1695Add -e EXPR to evaluate expressions w/out REPLDavid Raymond Christiansen 6a011d8Add docstrings to internally defined typesDavid Raymond Christiansen cfbb64fMerge branch 'idrisdoc' of github.com:PhilipRasmussen/Idris-dev into PhilipRasmussen-idrisdocDavid Raymond Christiansen e07c13dAdd :refine (:ref) command for refining a holeEdwin Brady a4295e3Merge pull request #1070 from david-christiansen/whocallsEdwin Brady f192d93Added comments on PTermPhilip Rasmussen 7bc8bfdAdd REPL commands for who calls whoDavid Raymond Christiansen 418a6b6Add :who-calls and :calls-who to IDESlaveDavid Raymond Christiansen e38b6c1Make the rest of erasure use ASTUtils.Matus Tejiscak dd44389Merged with masterPhilip Rasmussen a88053bAdd idris_postulates to IBC.Matus Tejiscak eedf489Remove collapsibility and forceability altogether.Matus Tejiscak 4957a33Make --nowarnreach the default (for now).Matus Tejiscak 644f093Require postulate unreachability instead of collapsibility.Matus Tejiscak bfd9900Add --nowarnreach.Matus Tejiscak 5b62302Add "detaggable" as an argument to OptInfo.Matus Tejiscak b5f219eRemove the Lazy flag entirely.Matus Tejiscak 7e633eeImprove reporting of accessibility errors.Matus Tejiscak b74ad4eReport names in accessibility check.Matus Tejiscak 9b80d0dAdd an "inaccessible" field to OptData.Matus Tejiscak ec85560Add accessibility recognition.Matus Tejiscak 5047cc5Add ErasedArg to PiOpts.Matus Tejiscak ad0dce1Invert the meaning of used/unused in CGInfo.Matus Tejiscak c074709Merge pull request #1040 from david-christiansen/issue/1019Edwin Brady 5f3627cShow terms more prettilyDavid Raymond Christiansen bfc3c3eMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-substTimo Petteri Sinnemäki 751a6eeComment cleanup.Timo Petteri Sinnemäki c78fb14Fixed errors; partially complete default arg subsTimo Petteri Sinnemäki 20e0bf4Merged with masterPhilip Rasmussen 3820110Ensure modules are loaded independentlyEdwin Brady d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen b1028f0TacImp script handling to various functions.Timo Petteri Sinnemäki e21b167Tiny tidying upPhilip Rasmussen