on ee32989 help sign in
all commits
ee32989Search in current elaboration stack for instancesEdwin Brady 2e6b5e0Fix universe checking errorEdwin Brady e95c877Make pattern matching consistent in lambda/letEdwin Brady 4175a7fCoverage checker should ignore hidden argumentsEdwin Brady 8789717Hide other unmatchable patternsEdwin Brady 0d8a153New way of dealing with unmatchable patternsEdwin Brady 684a578Completely replace ErrorT with ExceptTbmsherman 7b5f4aaFix visibility of imported thingsEdwin Brady fbcd643Check datatypes are not redefinedEdwin Brady 73e9c30Lifted TODO/FIXME from Idris/AbsSyntax.hsJan de Muijnck-Hughes f866fecUse Set for unique name checking for efficiencyEdwin Brady 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