Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 62
    • Issues 62
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • Open 9
  • Merged 361
  • Closed 34
  • All 404
  • add get_head tactic and use it in solve_proper_unfold
    !311 · created Jul 28, 2021 by Ralf Jung
    • MERGED
    • 6
    updated Jul 28, 2021
  • Generalize `map_filter_insert` so that it covers both the True and False case.
    !310 · created Jul 27, 2021 by Robbert Krebbers
    • MERGED
    • 6
    updated Jul 28, 2021
  • Use `SProp` to obtain better definitional equality for `pmap`, `gmap`, `gset`, `Qp`, and `coPset`
    !309 · created Jul 27, 2021 by Robbert Krebbers
    • MERGED
    • 45
    updated Dec 10, 2021
  • Add lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.
    !308 · created Jul 27, 2021 by Robbert Krebbers
    • MERGED
    • 0
    updated Jul 27, 2021
  • Clean up `empty{',_inv,_iff}` lemmas.
    !307 · created Jul 27, 2021 by Robbert Krebbers
    • MERGED
    • 26
    updated Jul 28, 2021
  • Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`
    !306 · created Jul 26, 2021 by Robbert Krebbers
    • MERGED
    • Approved
    • 7
    updated Jul 27, 2021
  • some lemmas about list submseteq
    !305 · created Jul 26, 2021 by Ralf Jung
    • MERGED
    • 26
    updated Jul 27, 2021
  • Add lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses.
    !304 · created Jul 24, 2021 by Robbert Krebbers
    • MERGED
    • 0
    updated Jul 24, 2021
  • solve_ndisj: handle goals containing _ ∖ _ ∖ _
    !303 · created Jul 22, 2021 by Ralf Jung
    • MERGED
    • 1
    updated Jul 23, 2021
  • `Params` and `Proper` instances for `curry` and friends
    !302 · created Jul 21, 2021 by Robbert Krebbers
    • MERGED
    • 8
    updated Jul 21, 2021
  • rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)
    !301 · created Jul 21, 2021 by Ralf Jung
    • MERGED
    • 2
    updated Jul 21, 2021
  • solve_ndisj: solve more goals involving chains of differences
    !300 · created Jul 21, 2021 by Ralf Jung
    • MERGED
    • 10
    updated Jul 21, 2021
  • alternative implementation of mk_evar that keeps naive_solver working
    !299 · created Jul 17, 2021 by Ralf Jung
    • MERGED
    • 11
    updated Jul 21, 2021
  • Mark gset methods as simpl never to stop `cbn` from unfolding them
    !298 · created Jul 17, 2021 by Paolo G. Giarrusso   S-waiting-for-author
    • MERGED
    • 16
    updated Jul 28, 2021
  • Swap `curry` and `uncurry` to be consistent with Haskell and friends.
    !297 · created Jul 16, 2021 by Robbert Krebbers
    • MERGED
    • 13
    updated Jul 20, 2021
  • Do not call `done` recursively when solving `is_Some`.
    !296 · created Jul 15, 2021 by Robbert Krebbers
    • MERGED
    • 7
    updated Jul 15, 2021
  • handle more goals in solve_ndisj
    !294 · created Jul 08, 2021 by Ralf Jung
    • MERGED
    • 14
    updated Jul 19, 2021
  • Make `done` work on `is_Some`.
    !293 · created Jul 03, 2021 by Robbert Krebbers
    • MERGED
    • 3
    updated Jul 15, 2021
  • add lookup_union_l
    !292 · created Jul 03, 2021 by Ralf Jung
    • MERGED
    • 3
    updated Jul 03, 2021
  • Fix priority of `Permutation_app'`.
    !291 · created Jun 29, 2021 by Robbert Krebbers
    • MERGED
    • 17
    updated Jul 15, 2021
  • Prev
  • 1
  • 2
  • 3
  • 4
  • 5
  • 6
  • 7
  • 8
  • 9
  • …
  • 19
  • Next