diff options
| author | Thomas Bauereiss | 2019-01-17 01:20:33 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-01-17 01:20:33 +0000 |
| commit | 7ebe7fe5a37959b9004548b4287dbfc1f6faa087 (patch) | |
| tree | ebb50f11d57eb1e95a492c7be1b5dd8e51b7e86e /lib/main.ml | |
| parent | 63fa9e0e2807e4b5fc3f825e6914a2fab5de37e3 (diff) | |
Work around an issue with type abbreviations in HOL
If we use the bitlist representation of bitvectors, the type argument in
type abbreviations such as "bits('n)" becomes dead, which confuses HOL;
as a workaround, expand type synonyms in this case.
Diffstat (limited to 'lib/main.ml')
0 files changed, 0 insertions, 0 deletions