git.iko.soy/Idris-dev
on 64bd27e help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
cdff1dbMerge pull request #1659 from edwinb/partial-evalEdwin Brady 8e6b636Optimisation optionsEdwin Brady 03f6913Partially evaluate type class dictionariesEdwin Brady e90316aSupport type errors in docstringsDavid Raymond Christiansen 6f9d433Parameters should be made 'static'Edwin Brady e890280Merge pull request #1619 from ahmadsalim/feature/renamevoidEdwin Brady 6e74e33Fix for pattern vars in transformsEdwin Brady edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi 37748ceAdd transformation rules for partial evaluationEdwin Brady 37292e1Save terms in docstringsDavid Raymond Christiansen e071c68EitherErr Applicative for Functor-Applicative-Monad_ProposalHeather 7e7368dStore kind in Pi bindersEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady ddced5cStore parameters in function typesEdwin Brady 44b38a6Fix implicits bugEdwin Brady 788f800Record import paths in ibcEdwin Brady 480024cRemove all the handle argumentsDavid Raymond Christiansen 1add7b7provide a Handle for IdeSlave, used to read from and write to (instead of hardcoded stdin/stdout) also send protocol-version message when the client connects also accept a single client connection when --ideslave-socket is provided (I don't see any reason to have multiple clients at all!)Hannes Mehnert 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