helm/www/lambdadelta/web/home/changes.tbl

   1 name "changes"
   2
   3 table {
   4   class "gray"
   5   [ "version" [ "aspect" [ "" "changes" ]]
   6   ]
   7
   8   class "orange"
   9   [ { "λδ-2B" + "(unreleased)" * }
  10     {
  11      [ [{ "equivalences" * }]
  12        { "+" "+" "+" "-" }
  13        { "equivalence for full rt-reduction (terms)"
  14          "equivalence for whd rt-reduction (terms)"
  15          "equivalence for extended rt-reduction (terms, referred lenvs, closures)"
  16          "syntactic equivalence (closures) removed"
  17        }
  18      ]
  19      [ [{ "weights" * }]
  20        { "+" }
  21        { "switch in primitive order relations for closures to enable the exclusion binder"
  22        }
  23      ]
  24      [ [{ "relocation" * }]
  25        { "" }
  26        { ""
  27        }
  28      ]
  29      [ [{ "syntax" * }]
  30        { "+" }
  31        { "exclusion binder for lenvs"
  32        }
  33      ]
  34      [ [{ "ground" * }]
  35        { "+" "*" "+" "-" }
  36        { "rt-transition counters"
  37          "generic reference transforming maps as streams of non-negative integers"
  38          "extensional equality, labelled transitive closures and streams"
  39          "non-negative integers with infinity removed"
  40        }
  41      ]
  42     }
  43   ]
  44
  45   class "orange"
  46   [ { "λδ-2A" + "(October 2014)" * }
  47     {
  48      [ [{ "equivalences" * }]
  49        { "+" }
  50        { "syntactic equivalence (selected lenvs, referred lenvs, closures)"
  51        }
  52      ]
  53      [ [{ "weights" * }]
  54        { "*" "-" }
  55        { "primitive order relations for closures"
  56          "complex weight (terms) removed"
  57        }
  58      ]
  59      [ [{ "relocation" * }]
  60        { "-" }
  61        { "level update functions removed"
  62        }
  63      ]
  64      [ [{ "syntax" * }]
  65        { "+" "+" "+" "-" "-" }
  66        { "polarized binders for terms"
  67          "non-negative integer global references for terms"
  68          "syntactic support for genvs with typed abstraction, abbreviation"
  69          "numbered sorts, application, type annotation removed from lenvs"
  70          "exclusion binder removed from terms and lenvs"
  71        }
  72      ]
  73      [ [{ "ground" * }]
  74        { "+" "+" }
  75        { "lists and non-negative integers with infinity"
  76          "library extension for transitive closures and booleans"
  77        }
  78      ]
  79     }
  80   ]
  81
  82   class "red"
  83   [ { "λδ-1A" + "(November 2006)" * }
  84     {
  85      [ [{ "equivalences" * }]
  86        { "" }
  87        { "equivalence for outer reduction (terms)"
  88        }
  89      ]
  90      [ [{ "weights" * }]
  91        { "" "" "" }
  92        { "order relations (terms, lenvs, closures) based on weights"
  93          "simple weights (terms, lenvs, closures)"
  94          "complex weight (terms)"
  95        }
  96      ]
  97      [ [{ "relocation" * }]
  98        { "" }
  99        { "level update functions"
 100        }
 101      ]
 102      [ [{ "syntax" * }]
 103        { "" "" }
 104        { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation"
 105          "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation" }
 106      ]
 107      [ [{ "ground" * }]
 108        { "" "" }
 109        { "finite reference transforming maps as compositions of basic ones"
 110          "library extension for logic and non-negative integers"
 111        }
 112      ]
 113     }
 114   ]
 115
 116 }
 117
 118 class "center" { 2 }