Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Branch: master
Commits on Oct 26, 2010
  1. IDesc: code alignment authored
  2. quotients: add legend for class authored
  3. ydtm: add Makefile authored
  4. ydtm: fix typos authored
Commits on Oct 21, 2010
  1. quotients note: use proper notation for quotient and class. authored
Commits on Oct 20, 2010
  1. notes: add Quotients documentation. authored
Commits on Sep 29, 2010
  1. Tactics.Matching: replace horrible solveEquation with a canTy-based i… authored
    This is broken, as documented in the file, but it works better than the old code. I will file a bug explaining the problems.
  2. Add instance HalfZip Elim and corresponding aspect authored
Commits on Sep 25, 2010
  1. added lambda calculus code to the manual authored
Commits on Sep 23, 2010
  1. icfp talk: backup my slides so far authored
  2. some corrections to the manual authored
Commits on Sep 22, 2010
  1. Search for recursive calls inside branches authored
    When looking for recursive call justification hypotheses in |seekLabel|, we can go inside branches by creating a fresh reference and switching on the branches (compare applying the hypothesis when going inside a Pi-type). If the branches are particularly nice, this might let us find a recursive call we would not otherwise spot.
  2. Stop elaborator from labelling inductive data types authored
    Now that we have the data and idata tactics, we do not need to label inductive data types when we elaborate them. This is good, because sometimes the elaborator would attach labels in the wrong places when doing generic programming.
    The IDesc elaboration/distillation/pretty-printing code has been extended to support unlabelled |IMu|s, and Desc has been tidied up a little.
  3. updated the downloads section to cabal authored
  4. added pigmode to the running epigram section of the manual authored
  5. added lookup and tabulate to the manual authored
  6. Features.Enum: implement induction principle for enumerations (issue … authored
    This should let us handle partial enumerations more easily, and we could replace the hard-coded switch operator with a definition that appeals to enumInduction. We still need a compiler definition for the new operator.
    The pretty-printing size of the numeric representation of enumerations (1 + e) has also been corrected.
Commits on Sep 21, 2010
  1. Tactics.Relabel: rewrite to use canTy for matching canonical construc… authored
    This means that we can write |con x| on the left-hand side, amongst other things.
  2. pigmode: comments coloring gets top priority

    Pierre-Evariste Dagand authored
Commits on Sep 20, 2010
  1. Test: port Levitation code (checkpoint)

    Pierre-Evariste Dagand authored
Commits on Sep 18, 2010
  1. test: add issue #109 test case, BugSubstEq.pig authored
  2. Test: fix the simpler(?) induction for IDesc authored
Commits on Sep 16, 2010
  1. Generic guarded fixpoint construction in Desc (and most of the constr… authored
    …uction for IDesc)
    Removed Below.pig and added DescFix.pig and IDescFix.pig. Both use a hack to handle mutual recursion with helper functions. The IDesc variant is incomplete (see comments in the file).
  2. NameResolution: fix non-exhaustive pattern in showEntries (issue 108) authored
Commits on Sep 13, 2010
  1. Distiller: ignore de Bruijn index on FAKE references (issue 87) authored
  2. Update test results for previous patch (issue 23, issue 101) authored
    Disable SimpleIInduction.pig; add results for Sort.pig but leave disabled because it is slow.
  3. Relabel: handle global parameters (issue 23) and applications (issue … authored
    …101) correctly
    Suppress the parameters in global scope (i.e. not in the current development) when relabelling, since they cannot be relabelled and to match the appearance of the programming problem. Allow applications and labelled calls in relabelling.
Commits on Sep 11, 2010
  1. EWAM: removed one redundant bquote authored
  2. pigmode red tags, Sort.pig cosmetics authored
  3. Cochon: rollback code re-use for reading commands.

    Pierre-Evariste Dagand authored
    Code re-use... Stop kidding yourself.
  4. pigmode: different handling of windows. Run Pig with comint.

    Pierre-Evariste Dagand authored
  5. pigmode: ignore trailing spaces. '--.*$' is a comment.

    Pierre-Evariste Dagand authored
  6. Merge authored
  7. pigmode: support multi-line inputs (looking for a terminating ';\n')

    Pierre-Evariste Dagand authored
Something went wrong with that request. Please try again.