diff options
| author | Thomas Bauereiss | 2018-12-13 20:37:36 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-12-13 20:37:36 +0000 |
| commit | cbd4eedf0d278572e70b04d9e9ef8750c4cae0a4 (patch) | |
| tree | 303cf5190261068cf74f558df90de47d8c5f652c /src/initial_check.ml | |
| parent | 7bbed580db0abeaa1acaa47610f01571ffe75ff4 (diff) | |
Remove redundant zero extensions more aggressively in mono rewrites
subrange_subrange_concat does a zero extension internally, so another
zero extension of its result is redundant and can lead to a type error
in Lem (because Lem's type system cannot calculate the length of the
intermediate result of subrange_subrange_concat).
Diffstat (limited to 'src/initial_check.ml')
0 files changed, 0 insertions, 0 deletions