Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
bcf29bb3
Commit
bcf29bb3
authored
Oct 15, 2021
by
Michael Sammler
Browse files
never simpl bool_decide
parent
089ad9e8
Pipeline
#55223
passed with stage
in 13 minutes and 56 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/lithium/base.v
View file @
bcf29bb3
...
...
@@ -23,6 +23,7 @@ Typeclasses Opaque is_Some.
Global
Opaque
rotate_nat_add
rotate_nat_sub
.
Typeclasses
Opaque
Z
.
divide
Z
.
modulo
Z
.
div
Z
.
shiftl
Z
.
shiftr
.
Arguments
bool_decide
:
simpl
never
.
Arguments
min
:
simpl
nomatch
.
Arguments
Z
.
testbit
:
simpl
never
.
...
...
Michael Sammler
@msammler
mentioned in commit
bd28ab82
·
Oct 15, 2021
mentioned in commit
bd28ab82
mentioned in commit bd28ab828a5415a8fc28bbec86fa26ea3c62152b
Toggle commit list
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment