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
ac6f5d18
Commit
ac6f5d18
authored
Nov 27, 2017
by
Robbert Krebbers
Browse files
Do not name constructor of `agree`; it should never be used.
parent
19649432
Pipeline
#5583
passed with stages
in 5 minutes and 59 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/agree.v
View file @
ac6f5d18
...
...
@@ -26,11 +26,10 @@ Proof.
Thus Ag(T) is not necessarily complete.
*)
Record
agree
(
A
:
Type
)
:
Type
:
=
Agree
{
Record
agree
(
A
:
Type
)
:
Type
:
=
{
agree_car
:
list
A
;
agree_not_nil
:
bool_decide
(
agree_car
=
[])
=
false
}.
Arguments
Agree
{
_
}
_
_
.
Arguments
agree_car
{
_
}
_
.
Arguments
agree_not_nil
{
_
}
_
.
Local
Coercion
agree_car
:
agree
>->
list
.
...
...
@@ -82,7 +81,7 @@ Instance agree_validN : ValidN (agree A) := λ n x,
Instance
agree_valid
:
Valid
(
agree
A
)
:
=
λ
x
,
∀
n
,
✓
{
n
}
x
.
Program
Instance
agree_op
:
Op
(
agree
A
)
:
=
λ
x
y
,
Agree
(
agree_car
x
++
agree_car
y
)
_
.
{|
agree_car
:
=
agree_car
x
++
agree_car
y
|}
.
Next
Obligation
.
by
intros
[[|??]]
y
.
Qed
.
Instance
agree_pcore
:
PCore
(
agree
A
)
:
=
Some
.
...
...
Robbert Krebbers
@robbertkrebbers
mentioned in issue
#114 (closed)
·
Nov 27, 2017
mentioned in issue
#114 (closed)
mentioned in issue #114
Toggle commit list
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