Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 186
    • Issues 186
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 18
    • Merge requests 18
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • 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 18
  • Merged 857
  • Closed 112
  • All 987

  • Subscribe to RSS feed
  • Avoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.
    !980 · created Aug 29, 2023 by Robbert Krebbers
    • 7
    updated Aug 30, 2023
  • Draft: experiment: use coq's ability to infer more canonical structures
    !972 · created Aug 11, 2023 by Ralf Jung
    S-blocked
    • 3
    updated Aug 28, 2023
  • Draft: Attempted fix for #539, solving slow type-checking of nested `●` terms
    !971 · created Aug 10, 2023 by Ike Mulder
    • 16
    updated Aug 28, 2023
  • generalize iso_cmra_mixin_restrict to a lemma that can also restrict the domain
    !970 · created Aug 10, 2023 by Ralf Jung
    • 5
    updated Aug 28, 2023
  • add option_fmap_dist_inj lemma
    !969 · created Aug 10, 2023 by Ralf Jung
    • 0
    updated Aug 10, 2023
  • have solve_proper exploit OfeDiscrete and LeibnizEquiv
    !968 · created Aug 08, 2023 by Ralf Jung
    • 0
    updated Aug 08, 2023
  • Draft: Add laws to allow "undiscarding" points-tos
    !960 · created Aug 01, 2023 by Johannes Hostert
    • 34
    updated Sep 22, 2023
  • generalize gmap_view for an arbitrary CMRA as values
    !959 · created Jul 27, 2023 by Ralf Jung
    • 1
    updated Aug 03, 2023
  • logically atomic triples: add private postcondition
    !956 · created Jul 26, 2023 by Ralf Jung
    • 1
    • 31
    updated Sep 21, 2023
  • Draft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.
    !953 · created Jul 24, 2023 by Robbert Krebbers
    • 7
    updated Aug 05, 2023
  • Make bi fields non-canonical
    !933 · created May 26, 2023 by Paolo G. Giarrusso
    • 31
    updated Jul 25, 2023
  • Draft: Improve validity information received from `iCombine`ing `own`s
    !930 · created May 25, 2023 by Ike Mulder
    • 22
    updated Aug 31, 2023
  • `Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.
    !916 · created Apr 30, 2023 by Robbert Krebbers
    S-waiting-for-author
    • 6
    updated Jul 25, 2023
  • add fixpoint lemmas for plain and absorbing
    !903 · created Apr 01, 2023 by William Mansky
    • 18
    updated Aug 05, 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
  • Renamed/added macros to iris.sty
    !851 · created Oct 12, 2022 by Jonas Kastberg
    S-waiting-for-author
    • 38
    updated Jul 25, 2023