Permalink
Commits on Jul 14, 2014
  1. javascript: whitespace

    committed Jul 14, 2014
  2. Merge pull request #1383 from david-christiansen/issue/1337

    Generate legal names for infix op lemmas
    david-christiansen committed Jul 14, 2014
  3. Merge pull request #1382 from david-christiansen/incomplete-quasiquote

    Properly type check quasiquotes
    david-christiansen committed Jul 14, 2014
  4. Remove unused code

    david-christiansen committed Jul 14, 2014
  5. Recheck quasiquotes

    This makes the elaborator for quasiquotes somewhat more strict, which
    prevents unknown names from sneaking in to quasiquotes as well as
    causing it to fail if not enough information is provided to solve implicits.
    david-christiansen committed Jul 14, 2014
Commits on Jul 12, 2014
  1. Fix scope/matching issues in proof scripts

    Need to treat appeals to tactics as independent calls to the elaborator,
    with known current scope, so don't add implicits until just before
    invoking the tactic, and add a final unify/match step to collect any
    missing implicits.
    edwinb committed Jul 12, 2014
Commits on Jul 11, 2014
  1. Remove dodgy unification hack

    Also need to recheck unification problems immediately after setting
    injective arguments, or we get strange results for disambiguation.
    Fixes #1372
    edwinb committed Jul 11, 2014
  2. Merge pull request #1380 from david-christiansen/no-trace-on-with

    Get rid of `trace` in error def
    david-christiansen committed Jul 11, 2014
  3. Merge pull request #1377 from puffnfresh/missing-instances

    Add Ord instance for Bool
    david-christiansen committed Jul 11, 2014
  4. Merge pull request #1379 from david-christiansen/paren-S-pat

    Add parens on generated S patterns
    david-christiansen committed Jul 11, 2014
  5. Don't do trace when `with` doesn't match

    This breaks IDESlave support. RE #879
    david-christiansen committed Jul 11, 2014
  6. Add parens on generated S patterns

    This fixes an issue where generated S patterns would sometimes not be
    parenthesized, leading to invalid patterns being generated. This
    occurred even in tutorial code, like Parity.
    david-christiansen committed Jul 11, 2014
  7. Add Ord instance for Bool

    puffnfresh committed Jul 11, 2014
Commits on Jul 10, 2014
  1. Merge pull request #1376 from Melvar/ideslave-let

    Allow :let in ideslave
    david-christiansen committed Jul 10, 2014
  2. Allow :let in ideslave

    Melvar committed Jul 10, 2014
  3. Merge pull request #1375 from david-christiansen/type-search-in-prover

    Make type search work in the prover
    david-christiansen committed Jul 10, 2014
  4. Make type search work in the prover

    This patch does two things:
    
    1. It adds support for a new prover command, :search, with the same
    syntax and semantics as the REPL command
    
    2. It makes :search work properly with IDESlave, enabling type search
    from the Emacs prover as well as enabling length-limits in the IRC bot
    again.
    david-christiansen committed Jul 10, 2014
Commits on Jul 9, 2014
  1. Allow :doc in prover

    This supports looking up documentation while proving. It's really most
    useful inside of an IDE.
    david-christiansen committed Jul 9, 2014
  2. Fix parameter propagation on CAFs

    Specifically, only propagate implicit parameters which are missing.
    Fixes #1370
    edwinb committed Jul 9, 2014
  3. Remove commented out code

    edwinb committed Jul 9, 2014
  4. Support multiple let bindings

    This sort of thing now works:
    
      test : Nat -> Nat
      test n = let foo = n
                   S k = plus foo foo
                  in k
    
    The bindings must be aligned, and the keyword 'in' (indented however you
    like within the 'test' block) terminates the list.
    
    Pattern match alternatives are also supported, for quickly catching
    failures:
    
      test2 : Nat -> Nat
      test2 n = let foo = n
                    S k = plus foo foo
                        | Z => 42
                  in k
    
    Fixes #1362
    edwinb committed Jul 9, 2014
  5. Keep type arguments of = when unelaborating

    This allows more informative error messages when the mismatch is in the
    type arguments to =.
    edwinb committed Jul 9, 2014
  6. Make prover better at IDESlave protocol

    Instead of returning strings that comprise results, return actions that
    complete them. This makes handling which requests are completed much easier.
    david-christiansen committed Jul 9, 2014
  7. Merge pull request #1369 from david-christiansen/prover-output-color

    Highlight prover output for ideslave
    edwinb committed Jul 9, 2014
  8. Merge pull request #1368 from Heather/clean

    windows executables should end with .exe
    edwinb committed Jul 9, 2014
  9. Highlight differing implicits in errors

    But only if there are otherwise no visible differences in the error
    edwinb committed Jul 9, 2014