git.iko.soy/Idris-dev
on 2aa64bd help sign in
2aa64bdCorrect documentation for --cpuBenjamin Saunders 2d8e573Move universe level check to after all modules are loaded ...otherwise it gets repeated needlessly for every moduleEdwin Brady 8f8ab98Remove unused syntax for 'InferRef' definitions Was only meant to be temporary! (InferRef are names in where clauses whose types are to be inferred)Edwin Brady 84c4db0Merge pull request #453 from Melvar/repl-initial-whitespaceEdwin Brady efa3f8fIgnore initial whitespace and comments in REPLMelvar Chen db84f5eMerge pull request #451 from Ralith/rts-cleanupEdwin Brady 6633a45Merge pull request #450 from raichoo/vimEdwin Brady 39e4241Merge pull request #448 from ziman/tutorial-typoEdwin Brady 3aa61b3Delete unused codeBenjamin Saunders c182c92Allow simple function types to be reflectedEdwin Brady 0cf168cvim: highlight metavars with quotesraichoo ebbdeadvim: highlight reflraichoo 6d7dc4eSimplify evaluator It tries to support too much, but since it's part of the kernel it should do as little clever stuff as possible. Now just normalises, simplifies or specialises, the latter two simply meaning that certain names are blocked from being reduced.Edwin Brady acc98c5Fix a typo in the tutorial.Matus Tejiscak dd12ac4Remove unused code in Evaluator plus some setting up for more control in inlining - VApp now takes two copies of its argument: one fully evaluated, one with names frozen. Plan is that dictionaries (in particular) will only unfold if doing so leads to further evaluation, so we need to keep both forms.Edwin Brady ecb42f0Resolve names/expand implicits inside refl Fixes #447Edwin Brady 680dcf7Increment IBC versionEdwin Brady d43a279Change TCGen flag to Dictionary, update evaluator accordinglyEdwin Brady 3fe14c7Calculate size allocation of BIGINT properlyEdwin Brady f226a47Make coverage checker look inside pairs/dependent pairs Fixes #446Edwin Brady 9d8916cMerge pull request #438 from andreas23/masterEdwin Brady 50e0bd1Merge pull request #445 from Melvar/masterEdwin Brady 9749544Merge pull request #444 from raichoo/javascriptEdwin Brady ca6c931Paper revisionsEdwin Brady 67c5fc9Remove nongeneric sum and product functionsMelvar Chen 108ee8ejavascript: refactored js codegenraichoo c2dce6cjavascript: refactoringraichoo 02f8b53Merge branch 'master' of github.com:edwinb/Idris-devEdwin Brady ecc3082A few more implementation paper edits Mainly shortening section 2Edwin Brady 7506102Merge pull request #440 from Melvar/Foldable_TraversableEdwin 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 922fdd1Try all names in refine to resolve ambiguity Fixes #426Edwin Brady e002347change traverse on Binder to a Traversable instanceMelvar Chen 614567fReadd toList as working on any FoldableMelvar Chen a449848Add Traversable instances for Maybe and (Vect n)Melvar Chen 545550fAdd Traversable and instance for ListMelvar Chen ac1c15bAdd traverse_ and sequence_ based on FoldableMelvar Chen d39f234Add instance Foldable MaybeMelvar Chen d4f173dAdd more folds and a Foldable instance for (Vect n)Melvar Chen 8c12b8cmake List use FoldableMelvar Chen c7fa2c7add FoldableMelvar Chen e940e39Add flags for gcc to treat signed ints in a predictable wayAndreas Bogk 3ad3bd6Merge pull request #429 from JasonGross/parallel-testsEdwin Brady 8a0e9d4Merge pull request #435 from JanBessai/SignedIntegerComparisonEdwin Brady 67739f0Merge pull request #434 from JanBessai/IndependentJavaRTSVersionEdwin Brady ff2b055Merge pull request #433 from Ralith/zext-inputs-are-unsignedEdwin Brady 8cbc717Merge pull request #432 from Ralith/cflagsEdwin Brady 0558972Fix parsing of indented blocks If there is no indentation, the block should be considered empty. This means empty parameters or using blocks are no longer allowed, which was always the intention, and empty data/instance/class declarations are allowed without needing an explicit {}. Fixes #437Edwin Brady e410ab3Fix missing cases in 'tldeclared' to allow class/instance in parameter blocks Fixes #436Edwin Brady