Detect difference between non-termination and interpretation error
Open
bug
- Dominant language
- Lean
- Stars
- 108
- Forks
- 32
- Avg merge
- 1d 1h
- Merged PRs (30d)
- 155
Description
`Interp T` is currently `Option (UBOr T)`. In particular, `none` is used both when the interpretation doesn't terminate (using `partial_fixpoint`), and also when there is an interpretation error.
We should change `Interp` to differenciate between the two cases.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.