git.iko.soy/Idris-dev
on bf4e535 help sign in
history ofsrc/Idris/DSL.hs
all commits
2e93a50Allow DSLs to be applied with $David Raymond Christiansen 3b5790cNamed lambda,let,pi in dsl blockChetan Taralekar 149c104Desugar do blocks inside of %runTacticsDavid Raymond Christiansen 2a1de7aExpand ! binds in tacticsDavid Raymond Christiansen 3c187ceBetter tracking of FC in implicit coercions / DSLDavid Raymond Christiansen e95c877Make pattern matching consistent in lambda/letEdwin Brady 1269791Keep type arguments of = when unelaboratingEdwin Brady 67f7373Support builds that doesn't use cabal for libs and rtsniklas 9993f3bAdd pi to overridable syntax in DSL blocksDavid Raymond Christiansen 8f93b00Syntax for failures in pattern matching let/<-Edwin Brady f6bebd3Proper pretty-printing of dependent pairsDavid Raymond Christiansen e80f871Annotate and colour pairs and () properlyDavid Raymond Christiansen d7b2913A simpler approach to handling name shadowingEdwin Brady 1c51b01EXPERIMENTAL: Disambiguate names in a blockEdwin Brady d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 5000aebAdd a Cabal libraryBrian McKenna 8e974c7Parser cleanup. Removing scaffolding parsers, rewrite PParser and IdeSlave from parsec to Haskell. No more parsec dependenciesAhmad Salim Al-Sibahi 3c32b65Whitespace cleanup.George Leontiev 57c8657Added column name to sourceAhmad Salim Al-Sibahi 9b74595Change '!' syntax and semantics to be uniformEdwin Brady 8c9ec38Added 'implicit bind' syntaxEdwin Brady 1bc3002Some Eff experimentation, adding a 'test' commandEdwin 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 96f4c54Add missing case for PEq to expandDo in DSL.hsEdwin Brady b543b29Allow names to be attached to provisional definitions lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent.Edwin Brady dcb9ca0Change meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.Edwin Brady 09f2abdFix let overloading bug with do blocksEdwin Brady 21c3a30Give up type class resolution soonerEdwin Brady dc3f0f9added dsl blocksEdwin Brady