git.iko.soy/Idris-dev
on 37845e4 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
dc69794Merge pull request #2245 from ahmadsalim/bug/fixequalityplicityDavid Christiansen 689e64bHighlight pi and lambda bindersDavid Raymond Christiansen 0cae95aRemoved equality from primNames, as it shouldn't be handle specially when adding implicits (the only current use).Ahmad Salim Al-Sibahi 2f6e736Fixes some string comparison that made sigma show incorrectly. Showing types of first component of sigma type.Ahmad Salim Al-Sibahi c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen 12bcfe4Allow type classes to have explicitly-named instance constructorsDavid Raymond Christiansen c538c34Merge remote-tracking branch 'refs/remotes/upstream/master' into agda-style-recordsDavid Raymond Christiansen 90127b3High-level if ... then ... else ... expressionDavid Raymond Christiansen c1cd201Merge remote-tracking branch 'refs/remotes/upstream/master' into agda-style-recordsDavid Raymond Christiansen 445f6a5Make PDirective IO monad freeNiklas Larsson 673a1fcTweak for types of case blocksEdwin Brady d6458bbAdd `{n} for quotations of the global name nDavid Raymond Christiansen e0b0516Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 53d5548Merge pull request #2167 from david-christiansen/bump-pprint-boundDavid Christiansen f238715Remove unused Show instanceDavid Raymond Christiansen ab9a2bcAdd a :browse command to the REPL and IDE equivalentDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 370939bMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady f987aecAdd info field to AppEdwin Brady 31f4c82Pretty-print bindings of MNs the same as references to MNsDavid Raymond Christiansen f1c6e39Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 7a8217aUse Set for boundNamesInEdwin Brady c3def79Rename Tactical to ElabDavid Raymond Christiansen 7d02904Progress towards defining functions in TacticalDavid Raymond Christiansen da8b88ashow incomplete term holes for listy constructorsJP Smith 5d269e3:exec can take an expression as an argumentEdwin Brady 5804426Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 9c13628Merge branch 'master' into agda-style-recordssualitu 26dba59Mergesualitu 0269d05More record stuff.Sune Alkaersig 0f86748Fix build errors with GHC 7.10.1. Fixes #2080Jan Stolarek 13a36a3Annotate functions as %hint for auto searchEdwin Brady fc02362Support externally defined primitivesEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady bbbe880Merged.Sune Alkærsig 9596463Merge branch 'master' into agda-style-recordsSune Alkærsig f36a8f7Revamped record elaboration.Sune Alkærsig 174395bMerge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 15737d9Trickiness with implicits in dependent classesEdwin Brady aa33865Merge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 1bf2731issue #2004 resolved by --consolewith cmd line paramAndreas Reuleaux 6d188c4Begin to use a sum type for post-elab IState tweaksDavid Raymond Christiansen 361efb5Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 147149bAdd 'determining parameters' for classesEdwin Brady c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen 75f6c2dAdd :core to the REPLDavid Raymond Christiansen bb013f0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 3d87454TT pretty-printing - also in elab debugDavid Raymond Christiansen aca1148Merge branch 'master' into agda-style-recordstdidriksen 6fe15eaAllow type providers to have docstringsAdam Sandberg Eriksson