Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
stdpp
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Monitor
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Iris
stdpp
Merge requests
Open
28
Merged
541
Closed
50
All
619
Actions
Subscribe to RSS feed
Toggle search history
Recent searches
You don't have any recent searches
Created date
Priority
Created date
Updated date
Closed date
Milestone due date
Popularity
Label priority
Title
add nil inversion lemma for take and drop
!621
·
created
9 hours ago
by
Kimaya Bedarkar
updated 9 hours ago
Forall exists Forall2 lemmas
!620
·
created
9 hours ago
by
Rudy Peterson
updated 9 hours ago
simplify and solve prefix
!619
·
created
9 hours ago
by
Rudy Peterson
updated 9 hours ago
list_to_set helper lemmas
!618
·
created
10 hours ago
by
Rudy Peterson
updated 9 hours ago
option_Forall2 lemmas
!616
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
option_Forall predicate
!615
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
Lemma map_to_list_update
!614
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
lemmas for map_Forall(2)
!613
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
lemmas for map_seq and map_seqZ
!612
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
fmap imap compose
!611
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
map alter lemmas
!610
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
kmap lemmas for map_to_list and list_to_map
!609
·
created
1 week ago
by
Rudy Peterson
updated 1 week ago
make eauto solve `is_Some None` as an assumption
!608
·
created
2 weeks ago
by
Sanjit Bhat
updated 2 weeks ago
Generate the [_CoqProject] file.
!604
·
created
1 month ago
by
Rodolphe Lepigre
updated 1 hour ago
Lookup lemmas for union list over finite maps
!603
·
created
1 month ago
by
Rudy Peterson
1
updated 1 month ago
Dune build compatible with Rocq 9.0.0.
!601
·
created
1 month ago
by
Rodolphe Lepigre
updated 1 month ago
Monad Laws
!600
·
created
1 month ago
by
Rudy Peterson
updated 1 month ago
Folding Map
!597
·
created
1 month ago
by
Rudy Peterson
updated 1 month ago
Zip Theorems
!596
·
created
1 month ago
by
Rudy Peterson
updated 3 weeks ago
Add `submsetseq` function
!593
·
created
2 months ago
by
Marijn van Wezel
updated 2 months ago
Previous
Next