Skip to content
Snippets Groups Projects

Notion of (in)finite predicates

Merged Notion of (in)finite predicates
robbert/pred_infinite into master
All threads resolved!
Merged Robbert Krebbers requested to merge robbert/pred_infinite into master
All threads resolved!

As discussed in iris!217 (merged)

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

Merge request reports

Merged by Robbert KrebbersRobbert Krebbers 6 years ago (Feb 21, 2019 8:33pm UTC)

Loading

Pipeline #14924 passed

Stage: build

Pipeline passed for c0e1e189 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung resolved all discussions

    resolved all discussions

  • Dan Frumin
  • Dan Frumin
    Dan Frumin @dfrumin ·
    Contributor

    I think this is good. The connections with infinite types can be established/studies in another mr I assume.

  • Robbert Krebbers resolved all discussions

    resolved all discussions

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Author Owner

    The connections with infinite types can be established/studies in another mr I assume.

    Yes, let's do that another day.

  • Robbert Krebbers mentioned in commit c0e1e189

    mentioned in commit c0e1e189

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers mentioned in merge request iris!217 (merged)

    mentioned in merge request iris!217 (merged)

    • Please register or sign in to reply