git.iko.soy/Idris-dev
on ced7733 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
c1968edFix parameter spotting in function typesEdwin Brady 29c02f4Fix scope/matching issues in proof scriptsEdwin Brady 6c39e35Fix parameter expansion in PEq caseEdwin Brady 1269791Keep type arguments of = when unelaboratingEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady dac312bAdd goal types to quasiquotes.David Raymond Christiansen e08a18dMerge remote-tracking branch 'refs/remotes/upstream/master' into quasiquoteDavid Raymond Christiansen ee11033Elaborate quasiquote patterns to something usefulDavid Raymond Christiansen f8ec244Elaborate qquotes in fresh proof stateDavid Raymond Christiansen 67f7373Support builds that doesn't use cabal for libs and rtsniklas d6c5b2bAdd semantic highlighting for postulatesDavid Raymond Christiansen 21124c3Merge remote-tracking branch 'upstream/master' into cantResolveAltsbmsherman 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman f15aaefPostpone implicit addition in case blocksEdwin Brady 94fc13cIDESlave support for :loadtoDavid Raymond Christiansen 50f63b5Make sensible implicit choices in :addlemmaEdwin Brady 89a975eImprove ideslave highlighting of primitivesDavid Raymond Christiansen 76c408fAdapt expandParamsD to new parameter docs field in PClassPaul Koerbitz 78ff448Bug fixing of induction bugsAhmad Salim Al-Sibahi 3c78dcbSimplify unused arg search.Matus Tejiscak 650b699Dummy commit to rerun a timeouted Travis buildTimo Petteri Sinnemäki bfc3c3eMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-substTimo Petteri Sinnemäki 8fcaa82Another wee comment adjustmentTimo Petteri Sinnemäki 751a6eeComment cleanup.Timo Petteri Sinnemäki c78fb14Fixed errors; partially complete default arg subsTimo Petteri Sinnemäki b696f28Make unique name generation much quickerEdwin Brady 3820110Ensure modules are loaded independentlyEdwin Brady d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki fb6a0edCoverage checker fixEdwin Brady f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen dd20facAdd semantic highlighting info for metavariablesDavid Raymond Christiansen b1028f0TacImp script handling to various functions.Timo Petteri Sinnemäki 569a30cMerge branch 'master' of github.com:edwinb/Idris-devTimo Petteri Sinnemäki 63342c7Some helper comments that'll be removed laterTimo Petteri Sinnemäki 8325cedAllow getting and setting options from IDESlaveDavid Raymond Christiansen 7faf4e8Show argument names in :docDavid Raymond Christiansen c5cb67cFix simple applicationEdwin Brady f707c76Merge remote-tracking branch 'upstream/master' into error-reflectionDavid Raymond Christiansen 3e401fbImprove error pretty-printingDavid Raymond Christiansen 992acb4Fix regression with data declarations in whereEdwin Brady 7437ebePrepared data structure of FC for spanning, and added the span of the last token parsed to IdrisAhmad Salim Al-Sibahi a7e6550Merge pull request #962 from david-christiansen/markdown-docsEdwin Brady d910c2cUse Markdown to represent docstringsDavid Raymond Christiansen 423b4c4Allow users to disable the auto-solve in the proverDavid Raymond Christiansen be57f4aFix unbound implicit rulesEdwin Brady c1ef938New syntax for documentation commentsDavid Raymond Christiansen c37de47Propagate parameters to recordsEdwin Brady 7b32c97No need to export primitives as metavariablesEdwin Brady 2df0a7fStore metavariables in ibc filesEdwin Brady af0171eProver commands for evaluation and typechecking expressionsDavid Raymond Christiansen