HomeIsabelle/Phabricator

Short constant index values can be put into the offset but leave larger and…

Authored by dcjm on Jul 14 2020, 9:07 AM.

Description

Short constant index values can be put into the offset but leave larger and negative values as an index.
Large values are possible but are more likely to be encountered in code that won't actually be executed.

Details

Committed
dcjmJul 14 2020, 9:07 AM
Parents
rPOLYMLc66cec192bdd: Modify test so that it works if int is IntInf.int.
Branches
Unknown
Tags
Unknown