Skip to content

Notion of (in)finite predicates

Robbert Krebbers requested to merge robbert/pred_infinite into master

As discussed in iris!217 (merged)

I have directly taken the opportunity to state set_finite using the new pred_finite.

Merge request reports