Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Commits on Dec 11, 2014
  1. @david-christiansen

    Merge pull request #1783 from jfdm/contrib/updates

    david-christiansen authored
    Updates to idrislang.sty
Commits on Dec 10, 2014
  1. Support for inductive-inductive types

    Add constructors to context immediately after elaborating, rather than
    adding the whole data type at once, so that later constructors can use
    them. Fixes #1757.
  2. @jfdm

    Several updates to idrislang.sty

    jfdm authored
    + Removal of numbers package option. Listing styles must be set either globally using `\lstset{}` or per code or listings environment options.
    + Addition of a beamer style.
    + Inclusion of the `:pprint` LaTeX formatting commands. No more need to copy everything from the result of `:pprint`, just the code snippet.
      + command chars for fancy verbatim has been set globally.
    + Option to change spacing command, useful for cases where line spacing is changed via different commands. For example: memoir has `\SingleSpacing`, setspace has `\singlespacing`.
Commits on Dec 9, 2014
  1. @jfdm

    Updates to idrislang.sty

    jfdm authored
  2. Remove -Werror in Output.hs due to ErrorT

    As far as I can tell, we can't replace ErrorT with ExceptT yet because
    there's a missing MonadException instance in Haskeline. Also, the
    dependencies we have set are causing a build failure on travis due to
    the -Werror.
    Proper fixes welcome! This is noted in issue #1780
  3. Check datatypes are not redefined

    We were checking, but only seeing if the type constructor was the same,
    which is not enough. Fixes #1776.
  4. Move Pair/Sigma into Builtins namespace

    Fixes #1775 (but there is still a related problem to address too,
    being #1776)
  5. Remove Type* on type of (.)

    We should leave this sort of thing until uniqueness types are more
    mature and we've experimented more outside the Prelude.
    Fixes #1777
  6. Fix for name clashes when applying transformations

    Fixes #1684, and most likely a lot of other partial evaluation problems.
    IBC version updated since the problem may show up in any library code
    that's currently built.
Commits on Dec 8, 2014
  1. Efficiency of unification

    Unification is trying to hard to unify things which are never going to
    work, and backtracking a lot. This stops that.
    Fixes #1219
  2. Merge pull request #1773 from JakobBruenker/master

    Added ":refine" to the autocompletions in the REPL
  3. Merge pull request #1770 from jfdm/fix/lift-todo-completion

    Lifted TODO/FIXME issues to the issue tracker for Completion.hs
  4. Merge pull request #1762 from bmsherman/improveParserErrors2

    Improve parser errors in dependent type signatures
Commits on Dec 7, 2014
  1. @raichoo

    Merge pull request #1774 from raichoo/master

    raichoo authored
    added IOExcept handler to FileIO effect
  2. @raichoo
  3. @JakobBruenker
Commits on Dec 5, 2014
  1. Add a default case for addShows

    The assumption that the argument lists are equal in length is a flawed
    one. Fixes #1765
  2. Avoid retrying unification problems constantly

    If solved metavariables do nothing to a unification problem, there's no
    point in trying it again - this can lead to a massive slowdown if
    there's a lot of evaluation in the type. Partially addresses #1219.
    Fixes #1716 on the way by tidying up type of updateProblems.
  3. @jfdm
Commits on Dec 4, 2014
  1. Merge pull request #1763 from ziman/show-vect

    Define `Show` instance for `Vect` via `toList`
  2. Merge pull request #1761 from bmsherman/dontDupErrors

    Reduce redundant 'specifically' clauses in errors
  3. Merge pull request #1755 from mattias-lundell/master

    Make tests work with sandboxes and fix GC statistics overflow
  4. Merge pull request #1712 from Melvar/remove-impossible

    Remove a no longer necessary `impossible`
  5. @ziman
  6. Need to resolve autos in each 'try' branch

    If the branch solves an implicit which makes the auto solvable, we need
    to try to resolve it straight away so we know whether the branch is
    valid or not. We need this especially when using 'try' to implement
    implicit coercions.
  7. Improvement for 'auto'

    Now proof search can be deferred if there are too many metavariables in
    the goal - previously in this case it would happily pick any old
    solution causing weird errors elsewhere in some cases.
Commits on Dec 3, 2014
  1. @bmsherman
  2. @bmsherman
  3. @bmsherman
Commits on Dec 1, 2014
  1. @david-christiansen

    Merge pull request #1756 from jonatack/patch-1

    david-christiansen authored
    Fix a few typos in the README
Commits on Nov 30, 2014
  1. @david-christiansen

    Merge pull request #1758 from david-christiansen/feature/case-delab

    david-christiansen authored
    Improve delaboration and pretty-printing for "case"
Something went wrong with that request. Please try again.