Skip to content
This repository

Sep 25, 2012

  1. Added simple library packaging system

    Now used for the prelude (see lib/base.ipkg)
    authored September 25, 2012

Sep 24, 2012

  1. Added --libdir option

    authored September 24, 2012

Sep 13, 2012

  1. Group EVAL/APPLY constructors

    authored September 14, 2012

Sep 04, 2012

  1. Added lazy application to IRTS

    authored September 04, 2012

Jun 15, 2012

  1. Quicker resolution of overloaded names

    By checking the name's type against the goal type rather than fully
    checking.
    authored June 15, 2012

May 30, 2012

  1. Added binding form to syntax rules (and updated tutorial accordingly)

    authored May 30, 2012

May 04, 2012

  1. Fix a tactic implicit bug when argument given explicitly

    authored May 04, 2012

Mar 07, 2012

  1. Work on implementation paper; tutorial fixes

    authored March 07, 2012

Feb 27, 2012

  1. Update dependencies and correct examples

    authored February 27, 2012

Feb 23, 2012

  1. Added backtick notation: e.g. x xs

    authored February 23, 2012

Feb 20, 2012

  1. Parse rule for big integers is broken

    authored February 20, 2012

Feb 14, 2012

  1. Chase type classes for longer

    authored February 14, 2012

Feb 06, 2012

  1. Fix let overloading bug with do blocks

    authored February 06, 2012

Feb 03, 2012

  1. Tutorial typos fixed

    authored February 03, 2012

Feb 02, 2012

  1. Some documentation updates

    authored February 02, 2012

Feb 01, 2012

  1. Fix silly error in termination checker :)

    authored February 01, 2012

Jan 31, 2012

  1. Some re-ordering of the tutorial

    authored January 31, 2012

Jan 27, 2012

  1. Added record test

    authored January 27, 2012
  2. Record projection

    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.
    authored January 27, 2012

Jan 26, 2012

  1. Made tutorial and examples consistent with latest library

    authored January 26, 2012

Jan 24, 2012

  1. Error message tinker

    authored January 24, 2012

Jan 16, 2012

  1. Update CHANGELOG

    authored January 16, 2012

Jan 12, 2012

  1. cabal changes

    authored January 12, 2012

Jan 07, 2012

  1. Debraced tutorial

    authored January 07, 2012

Jan 06, 2012

  1. Monad comprehension example

    authored January 06, 2012

Dec 30, 2011

  1. Some more tutorial adapted from old version

    authored December 30, 2011

Dec 20, 2011

  1. Added system module (getArgs, getEnv, exit)

    authored December 20, 2011
Something went wrong with that request. Please try again.