Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
c5f3fc77
Commit
c5f3fc77
authored
Feb 26, 2016
by
Robbert Krebbers
Browse files
Correct implicit arguments dec_agree.
parent
ae4262a1
Changes
1
Hide whitespace changes
Inline
Side-by-side
algebra/dec_agree.v
View file @
c5f3fc77
...
...
@@ -52,5 +52,6 @@ Proof. destruct x; by repeat (simplify_eq/= || case_match). Qed.
Lemma
dec_agree_op_inv
(
x1
x2
:
dec_agree
A
)
:
✓
(
x1
⋅
x2
)
→
x1
≡
x2
.
Proof
.
destruct
x1
,
x2
;
by
repeat
(
simplify_eq
/=
||
case_match
).
Qed
.
End
dec_agree
.
Arguments
dec_agreeRA
_
{
_
}.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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