git.iko.soy/Idris-dev
on d1663cc help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
16eee46Fix case split bug on complex nested patternsEdwin Brady 3c32b65Whitespace cleanup.George Leontiev 6adee80Add :apc for adding "proof style" declarationsEdwin Brady b7b55b7Allow hints to be given to proof searchEdwin Brady f869396Add :addmissing REPL commandEdwin Brady 53ce3ccProof search now also tries recursive callsEdwin Brady 5d2d5a7Failed proofsearch branch creates new metavariableEdwin Brady abf99a5Add proofsearch tactic, with :ps at the REPLEdwin Brady f34f0afBetter display of metavariable types in :tEdwin Brady 6456d6fAdd :makewith command at the REPLEdwin Brady 46256abAdd ':addclause' command at the REPLEdwin Brady d20f35cAdd --client optionEdwin Brady 66f4f9eExtend split/splitOnLine to cope with 'where/with'Edwin Brady 8c19e30Record internal name of 'with' functionsEdwin Brady 3729d95Add CaseSplit.hs and Command (not yet implemented)Edwin Brady bc0ebeeMerge branch 'feature/columntracking' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/columntrackingEdwin Brady 8b17db3Fixed flaw with FC dependency by making FC equality always return true. If any fc equality is needed just use FC' fc to convert. Fixes idris-lang/Idris-dev#550Ahmad Salim Al-Sibahi 57c8657Added column name to sourceAhmad Salim Al-Sibahi e4343cbSupport '!' at REPLEdwin Brady 8c9ec38Added 'implicit bind' syntaxEdwin Brady 50c66f9Added "if_valid" syntax rule for possibly failing EffectsEdwin Brady 55af041Merge pull request #540 from reynir/patch1Edwin Brady 23d10ceAdd missing patternReynir Reynisson ac33945Wrap Idris in an ErrorTDavid Christiansen 0e76ac9Remember whether implicits are machine generatedEdwin Brady 1bc3002Some Eff experimentation, adding a 'test' commandEdwin Brady 67fb9ccSplit Parser.hs into several filesEdwin Brady 3db1e91Added flag for error reflection extensionDavid Christiansen 39bc4c4Merge pull request #485 from lambdadomain/masterEdwin Brady c55f8c2Unification fix to avoid giving up on recoverable errorsEdwin Brady ed8114eUpdated dependencies and types for Haskell llvm bindings v3.3.8.1.lambdadomain fe20bf1Allow colour options from REPLDavid Christiansen 7c45129Colour theme in Idris REPL stateDavid Christiansen 2a0885eBetter representation and rendering of generated namesEdwin Brady af4fda7%flag directiveEdwin Brady ddc137eColourise some error messagesDavid Christiansen fddebcaHave :t colourise the left side of the colonDavid Christiansen c0342c7Add command line option to control REPL coloursDavid Christiansen 6c14565Move colourisation to a separate moduleDavid Christiansen 7226659Colourise implicit params with underlineDavid Christiansen f48e88fColourisation fix for replDavid Christiansen b762f14Basic colourisation in REPLDavid Christiansen ffb9ea9Semantic colouring of identifiers in REPLDavid Christiansen 1d4d226Optimise datatypes with one constructor and one argument No need to pack them up (because we're strict!) so just treat them as a newtype would be in Haskell.Edwin Brady 8eb2087Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325Edwin Brady 3aa61b3Delete unused codeBenjamin Saunders c182c92Allow simple function types to be reflectedEdwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin Brady 48d1105Added 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of automated proof by reflection.Edwin Brady fd9bd68Add '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.Edwin Brady