diff options
| author | Thomas Bauereiss | 2018-01-26 13:03:53 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-01-29 18:49:56 +0000 |
| commit | 2fdbc2993a9092121cf7f3eddeab688d83499553 (patch) | |
| tree | 783a069bb72e8832061f70a0ca44995c20704719 /src/initial_check.ml | |
| parent | 468bc2736ae82688eadc048e16ac6d01aa9ff78f (diff) | |
Output a few more type annotations for Lem
Allow pretty-printing of existential types, if the existentially quantified
variables do not actually appear in the Lem output. This is useful for the bit
list representation of bitvectors, as it will print the type annotation "list
bitU" for bitvectors whose length depends on an existentially quantified
variable.
Diffstat (limited to 'src/initial_check.ml')
0 files changed, 0 insertions, 0 deletions