Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Commits on Oct 7, 2012
  1. @edwinb

    Added --dumpc flag

    edwinb authored
Commits on Sep 25, 2012
  1. Added simple library packaging system

    Edwin Brady authored
    Now used for the prelude (see lib/base.ipkg)
Commits on Sep 24, 2012
  1. Added --libdir option

    Edwin Brady authored
Commits on Sep 13, 2012
  1. Group EVAL/APPLY constructors

    Edwin Brady authored
Commits on Sep 4, 2012
  1. Added lazy application to IRTS

    Edwin Brady authored
Commits on Jun 15, 2012
  1. Quicker resolution of overloaded names

    Edwin Brady authored
    By checking the name's type against the goal type rather than fully
    checking.
Commits on May 30, 2012
Commits on May 4, 2012
Commits on Mar 7, 2012
  1. Work on implementation paper; tutorial fixes

    Edwin Brady authored
Commits on Feb 27, 2012
  1. Update dependencies and correct examples

    Edwin Brady authored
Commits on Feb 23, 2012
  1. Added backtick notation: e.g. x xs

    Edwin Brady authored
Commits on Feb 20, 2012
  1. Parse rule for big integers is broken

    Edwin Brady authored
Commits on Feb 14, 2012
  1. Chase type classes for longer

    Edwin Brady authored
Commits on Feb 6, 2012
  1. Fix let overloading bug with do blocks

    Edwin Brady authored
Commits on Feb 3, 2012
  1. Tutorial typos fixed

    Edwin Brady authored
Commits on Feb 2, 2012
  1. Some documentation updates

    Edwin Brady authored
Commits on Feb 1, 2012
  1. Fix silly error in termination checker :)

    Edwin Brady authored
Commits on Jan 31, 2012
  1. Some re-ordering of the tutorial

    Edwin Brady authored
Commits on Jan 27, 2012
  1. Added record test

    Edwin Brady authored
  2. Record projection

    Edwin Brady authored
    Given a record, defined as follows, for example:
    
    record Foo : Nat -> Set where
          MkFoo : (name : String) ->
                  (things : Vect a n) ->
                  Foo n
    
    Functions 'name' and 'things' are generated to extract the record
    fields. 'implicit_n' and 'implicit_a' are generated to extract the
    implicit parts.
Commits on Jan 26, 2012
Commits on Jan 24, 2012
  1. Error message tinker

    Edwin Brady authored
Commits on Jan 16, 2012
  1. Update CHANGELOG

    Edwin Brady authored
Commits on Jan 12, 2012
  1. cabal changes

    Edwin Brady authored
Commits on Jan 7, 2012
  1. Debraced tutorial

    Edwin Brady authored
Commits on Jan 6, 2012
  1. Monad comprehension example

    Edwin Brady authored
Commits on Dec 30, 2011
  1. Some more tutorial adapted from old version

    Edwin Brady authored
Commits on Dec 20, 2011
  1. Added system module (getArgs, getEnv, exit)

    Edwin Brady authored
Something went wrong with that request. Please try again.