theories/base_logic/lib/own.v · b56835d0dcec6691d330c8b0d1bc40369f417c34 · Yixuan Chen / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

4054 commits behind the upstream repository.

6 years ago
b56835d0
Make uPred itself independent of BI interface and just prove primitive laws (like in master branch) · b56835d0
Ralf Jung authored 6 years ago
```
The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.
```
b56835d0

History
Make uPred itself independent of BI interface and just prove primitive laws (like in master branch)
Ralf Jung authored 6 years ago
```
The BI interface is then instantiated using these laws.  In particular, this
shows that the rules we claim to be admissible actually are.
```

own.v 8.66 KiB