diff options
| author | Hugo Herbelin | 2016-07-17 09:28:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-17 14:27:18 +0200 |
| commit | b976aa1e49579b7b50cfb140cbac8cb6f4c881a7 (patch) | |
| tree | 668c698299acdde06b9c809ff427b47d507c4d06 /interp/notation_ops.ml | |
| parent | 152aca663d76f0cfda21ddef880050f21bfe4995 (diff) | |
More examples of recursive notations, with emphasis in reference manual.
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) ..) ..).
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions