IntersectMBO / IntersectMBO/plutus
Adapt Behavioural proof Red-CC to SOPs in the metatheory
Open
Internal
Metatheory
status: triaged
- Dominant language
- Haskell
- Stars
- 1.6k
- Forks
- 508
- Avg merge
- 3d 10h
- Merged PRs (30d)
- 22
Description
Adapt the following proofs:
- [ ] Proof of lem62
- [ ] Proof of unwindVE
- [ ] Proof of refocus
- [ ] Proof of lem-→s⋆
- [ ] Proof of lemmaF'
- [ ] Proof of thm1b
- [ ] Proof of thm1bV
Contributor guide
Assessment
This issue has not been assessed yet.