Skip to content
GitLab

Notion of (in)finite predicates

Merged 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.