Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 21
    • Merge requests 21
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • Open 21
  • Merged 811
  • Closed 109
  • All 941
  • Add some missing internal validity and equivalence lemmas for dfrac, auth, agree and reservation_map
    !942 · created Jun 02, 2023 by Ike Mulder
    • 6
    updated Jun 03, 2023
  • Added missing reflexivity, symmetry, transitivity lemmas on ↔, →, -∗ and ∗-∗
    !941 · created Jun 01, 2023 by Ike Mulder
    • 5
    updated Jun 02, 2023
  • add test for iInv with accessor variables
    !937 · created May 30, 2023 by Ralf Jung
    • 0
    updated May 30, 2023
  • Make bi fields non-canonical
    !933 · created May 26, 2023 by Paolo G. Giarrusso
    • 19
    updated Jun 03, 2023
  • Use Ltac2 to avoid unrolling tactic notations with lists.
    !931 · created May 26, 2023 by Janno
    • 3
    • 14
    updated May 31, 2023
  • Draft: Improve validity information received from `iCombine`ing `own`s
    !930 · created May 25, 2023 by Ike Mulder
    • 20
    updated Jun 03, 2023
  • make lock spec a Class
    !929 · created May 21, 2023 by Ralf Jung
    • 0
    updated May 21, 2023
  • Add Fractional instance for AsFractional
    !926 · created May 11, 2023 by Isaac van Bakel
    • 33
    updated May 31, 2023
  • Show that for non-step indexed BIs, <pers> can trivially be inhabited.
    !925 · created May 05, 2023 by Robbert Krebbers
    • 14
    updated May 12, 2023
  • Add reference-counting reader-writer lock implementation
    !923 · created May 05, 2023 by Isaac van Bakel
    • 37
    updated May 31, 2023
  • `Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.
    !916 · created Apr 30, 2023 by Robbert Krebbers
    • 5
    updated May 02, 2023
  • Draft: Add a Strategy command for ucmra projections
    !907 · created Apr 19, 2023 by Ike Mulder
    • 10
    updated May 02, 2023
  • add fixpoint lemmas for plain and absorbing
    !903 · created Apr 01, 2023 by William Mansky
    S-waiting-for-review
    • 10
    updated May 30, 2023
  • Draft: parameterize the algebra folder by the stepindex type for integration with Transfinite Iris
    !888 · created Feb 05, 2023 by Lennard Gäher
    • 1
    • 74
    updated May 31, 2023
  • WIP: Step Update modality demonstration
    !887 · created Jan 30, 2023 by Jonas Kastberg
    • 1
    • 0
    updated May 26, 2023
  • get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays
    !883 · created Jan 12, 2023 by Ralf Jung
    • 4
    updated Jan 12, 2023
  • Added fupd_plain_soundness_no_lc_strong
    !857 · created Oct 25, 2022 by Jonas Kastberg
    S-waiting-for-author
    • 55
    updated Mar 23, 2023
  • Renamed/added macros to iris.sty
    !851 · created Oct 12, 2022 by Jonas Kastberg
    S-waiting-for-author
    • 37
    updated Mar 24, 2023
  • Draft: move bi_persistently_emp out of BI interface, and get a basic proof mode working again
    !843 · created Aug 13, 2022 by Ralf Jung
    • 32
    updated May 10, 2023
  • Make* class tweaks
    !842 · created Aug 13, 2022 by Ralf Jung
    S-blocked
    • 39
    updated Aug 16, 2022
  • Prev
  • 1
  • 2
  • Next