Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added a test for #4765 (an example of printing abbreviation with binders). | 2017-05-20 | |
| | |||
* | Taking into account binding patterns when agglutinating sequences of binders. | 2016-07-19 | |
| | | | | | Supporting accordingly printing of sequences of binders including binding patterns. | ||
* | Notations: fixing multiple binders used as terms in reverse order. | 2016-07-19 | |
| | |||
* | A new step on using alpha-conversion in printing notations. | 2016-07-18 | |
| | | | | | | | A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns). | ||
* | Partial fix to #4592 (notation requiring alpha-conversion for printing). | 2016-07-17 | |
| | |||
* | More examples of recursive notations, with emphasis in reference manual. | 2016-07-17 | |
| | | | | | | | | | | | | | Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..). | ||
* | Fixing a bug in recognizing a recursive pattern of notations | 2016-07-17 | |
| | | | | immediately in the scope of another recursive pattern. | ||
* | Fixing interpretation of notations w/ opposite instances of a recursive pattern. | 2016-07-17 | |
| | |||
* | Fixing printing of notations with several instances of a recursive pattern. | 2016-07-17 | |