diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-04-17 18:40:59 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2018-04-18 03:43:32 -0400 |
| commit | c574d7ecbd4633ddb3116a71d49ec180526ee8dc (patch) | |
| tree | bcb63da6cd6e811ed35fce2f681098a4cfc1c245 /src | |
| parent | bad2d2aaa49cc0ea7a77c24655204964a4f25d2b (diff) | |
Add a Z.cast2 case to bounds extraction
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 63f176b37..ab1580026 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -5582,6 +5582,7 @@ Module Compilers. => fun '((x, f) : ZRange.type.option.interp tx * (ZRange.type.option.interp tx -> ZRange.type.option.interp tC)) => f x | ident.Z_cast range => fun _ => Some range + | ident.Z_cast2 (r1, r2) => fun _ => (Some r1, Some r2) | ident.primitive type.Z v => fun _ => Some r[v~>v]%zrange | ident.nil _ => fun _ => Some nil |