Skip to content
Snippets Groups Projects
Commit 2353a354 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Also update proof_guide.

parent ee9b400b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 2 deletions
docs/proof_guide.md
+ 1
− 2
View file @ 2353a354
...@@ -99,10 +99,9 @@ for further details on `libG` classes). For example, the STS library is ...@@ -99,10 +99,9 @@ for further details on `libG` classes). For example, the STS library is
parameterized by an STS and assumes that the STS state space is inhabited: parameterized by an STS and assumes that the STS state space is inhabited:
```coq ```coq
Class stsG Σ (sts : stsT) := { Class stsG Σ (sts : stsT) := {
sts_inG : inG Σ (stsR sts); #[local] sts_inG :: inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts); sts_inhabited :> Inhabited (sts.state sts);
}. }.
Local Existing Instance sts_inG.
``` ```
In this case, the `Instance` for this `libG` class has more than just a `subG` In this case, the `Instance` for this `libG` class has more than just a `subG`
assumption: assumption:
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment