git.iko.soy/Idris-dev
on 02fa360 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
a807a34Remove the unused arg from lookup functionsDavid Christiansen ea6bb9aMerge branch 'ImprovedReflection' of https://github.com/JanBessai/Idris-dev into JanBessai-ImprovedReflectionEdwin Brady c1a4eacFull TT reflection and reificationJan Bessai 75e0141add command to change current directoryHannes Mehnert ab498e9Add syntax for language extensions and turn off type providers by defaultDavid Christiansen 161ef3dMerge remote-tracking branch 'upstream/master' into providersDavid Christiansen d81e2edAdd clauses to declared and defined.Sam T 228ffdbquiet mode: for editorsraichoo db5973bAdded rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v.Edwin Brady 3a80954%dynamic now works from IBC filesDavid Christiansen 3262127Dynamically load C libraries in REPLDavid Christiansen 0f49abcAdded first steps in type providersDavid Christiansen 306a451Reformat existing comments for Haddock and add Haddock commentsDavid Christiansen 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady c020e50javascript: split javascript and node targetraichoo d53fccfMerge pull request #180 from david-christiansen/completion-workEdwin Brady 053708aMerge pull request #176 from david-christiansen/completionEdwin Brady 0970f01Disentangle Haskeline from the internals IdrisDavid Christiansen 4ae0450Remove old code, tinker with section 4Edwin Brady e49ab72Reorder the monad transformers in the Idris monad to allow completionDavid Christiansen 2a13be4Distinguish parameters and indices internally in data types This doesn't do anything, yet, but will become important soon!Edwin Brady 265d9a4Improve elaboration efficiency by cutting down on excessive backtrackingEdwin Brady 57628ffMerge pull request #146 from raichoo/javascriptEdwin Brady 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady 12dcee5Merge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascriptIrene Knapp 06fffa3JavaScript stuff.Irene Knapp 8d83f38Abstract matched terms from goal type in with clauses (like 'magic with' in Agda)Edwin Brady dd5001fmake TT aware of Set -> Typeraichoo 7fefa89PSet -> PTyperaichoo e4da568Take more care when expanding names in nested parameter blocksEdwin Brady 2c58ebaFix elaboration of higher order dependent function types Fixes issue #116Edwin Brady e3d393cAdded the ability to dump bytecode to a fileDaniel Waterworth c10146bLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call.Edwin Brady f833918(Experimental) Create deferred definitions by applicationEdwin Brady e23c029Allow type annotations on let tacticEdwin Brady b1cdd04Added postulate declarations postulate foo : type -- 'type' must return something of a collapsible type, i.e. a type with at most one instancei determined entirely by the indices, to ensure that it is unused at run-time.Edwin Brady 0c33cf1fixed bug in showImpraichoo 40ce0cabetter fixity error messageraichoo f50f006Expand backend control options and infrastructureBenjamin Saunders 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady af66f25Added 'mutual' blocks Effect is to elaborate all types in the block before elaborating definitionsEdwin Brady 895b323Allow forward declaration of data structures To support induction-recursion and mutual data definitions Syntax is as a normal data declaration, but without the 'where' or '=' sectionsEdwin Brady 7438e0fDocument --warnpartial Behaviour fixed so that it doesn't report declared partial functionsEdwin Brady 665676bAdded :l and :m commands to REPLEdwin Brady 15fc297Merge branch 'master' of https://github.com/edwinb/Idris-devJason Dagit a41fe5bUse strict StateTJason Dagit 9affb75Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possibleEdwin Brady 54ad219Add size change termination Now deals with recursive functions (still only simple structural size changes spotted, however)Edwin Brady ebb75fbCalculate size change graphsEdwin Brady