diff options
| author | Hugo Herbelin | 2020-07-28 23:47:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-18 11:28:45 +0100 |
| commit | ca0e42c0ff9e5cebb734bcb59065a4f55ae4aa4e (patch) | |
| tree | 9da6b68e6bd56ced9247ba2135385be8dba86679 /kernel/float64_31.ml | |
| parent | 396de348a4daa2ae752bed8c75a9ecacb4dcd579 (diff) | |
In recursive notations, accept partial application over the recursive pattern.
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
Diffstat (limited to 'kernel/float64_31.ml')
0 files changed, 0 insertions, 0 deletions