git.iko.soy/Idris-dev
on 10d4cd6 help sign in
10d4cd6javascript: hardwired apply lookuptableraichoo feafceajavascript: apply lookuptableraichoo ce6bd98javascript: minor cleanupraichoo fbeeb45javascript: whitespaceraichoo e5d412ejavascript: added lookuptable namespaceraichoo a8abc5ajavascript: EVAL lookup tableraichoo 8cd9f56javascript: get rid of translateParameterraichoo 3d72873javascript: factor out jsDeclraichoo 186cc36javascript: factor out translateCaseraichoo 3109b51javascript: factor out translation of declsraichoo 954dd00Merge pull request #457 from Ralith/patch-1Edwin Brady 417f040Merge pull request #455 from Ralith/atomic-allocsEdwin Brady 2aa64bdCorrect documentation for --cpuBenjamin Saunders 2f8a33aUse atomic allocations when safe in LLVM codegen.Benjamin 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