diff options
| author | Brian Campbell | 2018-12-27 20:00:56 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-12-27 20:00:56 +0000 |
| commit | 2c887e7d01331d3165120695594eac7a2650ec03 (patch) | |
| tree | 0de8d2a88156fde59a72a0f9c5483b7c62f2d147 /language/bytecode.ott | |
| parent | 1940388163a9379cd6c157f3636439a93c5d4b67 (diff) | |
Coq: avoid putting ambiguous numeric literals in Coq output
There are situations when we really want a more refined expression,
such as 8 * n instead of 64 (when we know n = 8 from a case split), but
we might not be able to generate it. For now we generate an underscore
and let Coq figure it out from the context.
Diffstat (limited to 'language/bytecode.ott')
0 files changed, 0 insertions, 0 deletions