Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

S

stdpp
- Activity
- Members
- Labels
- Issues
- Issue boards
- Milestones
- Wiki
- Releases
- Model registry
- Service Desk

Snippets Groups Projects

!450

Cancellation for multiplication on `nat`.

Review changes
Download
Patches
Plain diff

Merged Cancellation for multiplication on `nat`.

robbert/mul_reg into master

Overview 1
Commits 2
Pipelines 2
Changes 2

Merged Robbert Krebbers requested to merge robbert/mul_reg into master 2 years ago

Overview 1
Commits 2
Pipelines 2
Changes 2

Coq's stdlib has these lemmas for Z, but those for nat are missing. We use the naming scheme of Coq's stdlib.

Edited 2 years ago by Robbert Krebbers

Merge request reports

Activity

Filter activity

Approvals
Assignees & reviewers
Comments (from bots)
Comments (from users)
Commits & branches
Edits
Labels
Lock status
Mentions
Merge request status
Tracking

Please register or sign in to reply

0 Assignees

0 Reviewers

Request review from

Loading

Labels

0

None

0

None

Select labels

Manage project labels

Milestone

None

None

None

Time tracking

No estimate or time spent

0

0 Participants

Loading