diff options
| author | Pierre Roux | 2020-09-30 13:13:25 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | e3593abd322acb59c512b5f2f776091546b38887 (patch) | |
| tree | d00d74dd36b34a41ab42ab585227a01657107fb2 /interp/notation.ml | |
| parent | da7787ff4f1b5192b5465ca17ece64f5ebd4f72a (diff) | |
[refman] Add an example for number notations
As suggested by Jim Fehrle while reviewing #12218
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions