Skip to content

Let `iProp` refer to `uPred ... : Type` instead of `uPredO ... : ofeT`

Robbert Krebbers requested to merge ci/robbert/iprop_structures into master

This has two advantages:

  • It is more consistent with respect to the rest of the development. Elsewhere we use the O suffix for the OFE variant and the version without suffix for the Type variant.
  • It gives a minor speedup of 1.72% overall on LambdaRust, with peaks of 5.77% for individual files. See here.

This MR breaks backwards compatibility, but the number of changes needed are minor. See here for LambdaRust.

Edited by Robbert Krebbers

Merge request reports