|
|
|---|
|
|
|
|---|
(Beta) Generate theorems relating the result of an updater visitor to the input object
If you have a simple visitor that updates some object by a simple transform such as stripping out some field,this can automatically prove rewrite rules such as, e.g., an accessor of the transform of some object equals the transform of the accessor of the object. Not yet tested in more complex cases. It generates such theorems for all types for which the visitor has been defined.