git.iko.soy/Idris-dev
on ee8fce0 help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen 40d094dExpose equality proofs in with ruleEdwin Brady b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen ef954e1Fix the new totality testDavid Raymond Christiansen 8096500Add %used pragmaEdwin Brady 60e4921Relax lower bound on mtlEric Mertens c729d2fSupport scoped type class constraintsEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 17fe233Add scoped implicit argument to PiEdwin Brady cad3b02Eat less memory by sharing namesEdwin Brady 2ec25c2Do more forcing in IBCEdwin Brady 7c34217Allow class constraints to be namedEdwin Brady 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