git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/ElabTerm.hs
all commits
e890280Merge pull request #1619 from ahmadsalim/feature/renamevoidEdwin Brady 2878ff3Solve more implicits before 'case' elaborationEdwin Brady edb9980Removed '_|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match upAhmad Salim Al-Sibahi a4faccbMerge pull request #1570 from jfdm/fixme/code-deletionDavid Christiansen cf3c47dRemoved dead commented out code.Jan de Muijnck-Hughes 7383b1cSupport nested quasiquotationDavid Raymond Christiansen 6faa1abRenaming of built-in datatypes works finallyAhmad Salim Al-Sibahi d3660edDon't pass used unique variables to metavarsEdwin Brady 7e7368dStore kind in Pi bindersEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady 9ceece1EXPERIMENTAL uniqueness typesEdwin Brady 42c694cMore efficiency improvementsEdwin Brady 2418336Save some allocations in updateSolvedEdwin Brady ab36099Use a zipper-like proof stateEdwin Brady 382542aAdd %no_implicit directiveEdwin Brady bc34332Improve quasiquote patterns for MNDavid Raymond Christiansen c41b605Update reflection code to current core language.David Raymond Christiansen 84b172aAdd tactics "skip" and "fail"David Raymond Christiansen 9242f46Resolve default Integer as late as possibleEdwin Brady 4d62d30x = y now tries homogeneous equality firstEdwin Brady adb59d0Resolve class instances under let bindingsEdwin Brady 90bb76dRemove unused codeDavid Raymond Christiansen d5411e2Recheck quasiquotesDavid Raymond Christiansen 29c02f4Fix scope/matching issues in proof scriptsEdwin Brady 8ed343bRemove dodgy unification hackEdwin Brady 6c39e35Fix parameter expansion in PEq caseEdwin Brady 1269791Keep type arguments of = when unelaboratingEdwin Brady 5ffef89Type class resolution fixEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady dac312bAdd goal types to quasiquotes.David Raymond Christiansen ae5c48aFix type error in generated quasiquote patternsDavid Raymond Christiansen 1153028Update comments to fit the state of the codeDavid Raymond Christiansen ee11033Elaborate quasiquote patterns to something usefulDavid Raymond Christiansen 36785b5Allow reflecting types with quasiquote patternsDavid Raymond Christiansen 1ecd340Support simple quasiquote patternsDavid Raymond Christiansen 6a5a1f3Initial support for unquotesDavid Raymond Christiansen f8ec244Elaborate qquotes in fresh proof stateDavid Raymond Christiansen 766b955Elaborate quasiquotesDavid Raymond Christiansen 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi e91819cFinal cleanup/check of case tactic implementationAhmad Salim Al-Sibahi 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi a0b05e2Allow induction on terms instead of simply namesAhmad Salim Al-Sibahi 9c59a19Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 921b766Fix name propagation in error messagesEdwin Brady 21124c3Merge remote-tracking branch 'upstream/master' into cantResolveAltsbmsherman 282abc8Enable pretty printing of CantResolveAlts errors.bmsherman 9907240Add new Err constructor to disambiguate the CantResolveAlts constructor.bmsherman 2a0056aNew matching rule for solving simple functionsEdwin Brady 41f921fUnify more things!Edwin Brady f15aaefPostpone implicit addition in case blocksEdwin Brady