git.iko.soy/Idris-dev
on cfe250a help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
e07c13dAdd :refine (:ref) command for refining a holeEdwin Brady a4295e3Merge pull request #1070 from david-christiansen/whocallsEdwin Brady 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 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 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 a724531Merge pull request #1001 from david-christiansen/doc-arg-namesEdwin Brady 7faf4e8Show argument names in :docDavid Raymond Christiansen 9c99a07Add 'covering' function optionEdwin Brady e9ef380Support text formatting in docstringsDavid Raymond Christiansen 15aebc9Add highlighting for keywords in interpreter outputDavid Raymond Christiansen 1921424Add :apropos command to REPLDavid Raymond Christiansen 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi db306caMerge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/parserspanningAhmad Salim Al-Sibahi a7e6550Merge pull request #962 from david-christiansen/markdown-docsEdwin Brady 2d79c85Merge pull request #958 from david-christiansen/reflection-reflectionEdwin Brady d910c2cUse Markdown to represent docstringsDavid Raymond Christiansen 8f93b00Syntax for failures in pattern matching let/<-Edwin Brady 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen a7217f1Tweak scoping rules in instance generationEdwin Brady 419b35cAdded span in parser stateAhmad Salim Al-Sibahi c1ef938New syntax for documentation commentsDavid Raymond Christiansen bd744f1Propagate function name to tacticsEdwin Brady 8319e27Merge pull request #937 from david-christiansen/postulate-providersEdwin Brady 2df0a7fStore metavariables in ibc filesEdwin Brady 0875310Control whether provider decls accept postulatesDavid Raymond Christiansen 151d4efMerge pull request #924 from david-christiansen/prover-new-commandsEdwin Brady af0171eProver commands for evaluation and typechecking expressionsDavid Raymond Christiansen c733a8fParser warnings; especially for invalid doc commentsDavid Raymond Christiansen