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
cabdcfc3
Unverified
Commit
cabdcfc3
authored
Mar 17, 2022
by
Paolo G. Giarrusso
Browse files
Hide preG instances
parent
dbe95c90
Changes
5
Hide whitespace changes
Inline
Side-by-side
docs/resource_algebras.md
View file @
cabdcfc3
...
...
@@ -123,9 +123,10 @@ Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
}.
Local
Existing
Instances
gen_heapGpreS_heap
.
Class
gen_heapGS
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
GenHeapGS
{
gen_heap_inG
:
>
gen_heapGpreS
L
V
Σ
;
gen_heap_inG
:
gen_heapGpreS
L
V
Σ
;
gen_heap_name
:
gname
;
}.
Local
Existing
Instance
gen_heap_inG
.
```
The trailing
`S`
here is for "singleton", because the idea is that only one
instance of
`gen_heapGS`
ever exists. This is important, since two instances
...
...
iris/base_logic/lib/gen_heap.v
View file @
cabdcfc3
...
...
@@ -73,10 +73,11 @@ Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
Local
Existing
Instances
gen_heapGpreS_meta_data
gen_heapGpreS_heap
gen_heapGpreS_meta
.
Class
gen_heapGS
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
GenHeapGS
{
gen_heap_inG
:
>
gen_heapGpreS
L
V
Σ
;
gen_heap_inG
:
gen_heapGpreS
L
V
Σ
;
gen_heap_name
:
gname
;
gen_meta_name
:
gname
}.
Local
Existing
Instance
gen_heap_inG
.
Global
Arguments
GenHeapGS
L
V
Σ
{
_
_
_
}
_
_
.
Global
Arguments
gen_heap_name
{
L
V
Σ
_
_
}
_
:
assert
.
Global
Arguments
gen_meta_name
{
L
V
Σ
_
_
}
_
:
assert
.
...
...
iris/base_logic/lib/gen_inv_heap.v
View file @
cabdcfc3
...
...
@@ -36,9 +36,10 @@ Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
Local
Existing
Instance
inv_heapGpreS_inG
.
Class
inv_heapGS
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
Inv_HeapG
{
inv_heap_inG
:
>
inv_heapGpreS
L
V
Σ
;
inv_heap_inG
:
inv_heapGpreS
L
V
Σ
;
inv_heap_name
:
gname
}.
Local
Existing
Instance
inv_heap_inG
.
Global
Arguments
Inv_HeapG
_
_
{
_
_
_
_
}.
Global
Arguments
inv_heap_name
{
_
_
_
_
_
}
_
:
assert
.
...
...
iris/base_logic/lib/proph_map.v
View file @
cabdcfc3
...
...
@@ -14,10 +14,11 @@ Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
Local
Existing
Instances
proph_map_GpreS_inG
.
Class
proph_mapGS
(
P
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
P
}
:
=
ProphMapGS
{
proph_map_inG
:
>
proph_mapGpreS
P
V
Σ
;
proph_map_inG
:
proph_mapGpreS
P
V
Σ
;
proph_map_name
:
gname
}.
Global
Arguments
proph_map_name
{
_
_
_
_
_
}
_
:
assert
.
Local
Existing
Instances
proph_map_inG
.
Definition
proph_map
Σ
(
P
V
:
Type
)
`
{
Countable
P
}
:
gFunctors
:
=
#[
ghost_map
Σ
P
(
list
V
)].
...
...
iris/base_logic/lib/wsat.v
View file @
cabdcfc3
...
...
@@ -15,7 +15,7 @@ Module invGS.
}.
Class
invGS
(
Σ
:
gFunctors
)
:
Set
:
=
InvG
{
inv_inG
:
>
invGpreS
Σ
;
inv_inG
:
invGpreS
Σ
;
invariant_name
:
gname
;
enabled_name
:
gname
;
disabled_name
:
gname
;
...
...
@@ -30,6 +30,7 @@ Module invGS.
Proof
.
solve_inG
.
Qed
.
End
invGS
.
Import
invGS
.
Local
Existing
Instances
inv_inG
invGpreS_inv
invGpreS_enabled
invGpreS_disabled
.
Definition
invariant_unfold
{
Σ
}
(
P
:
iProp
Σ
)
:
later
(
iProp
Σ
)
:
=
Next
P
.
...
...
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