diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-05 15:44:38 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-05 15:44:38 +0000 |
| commit | b7227fb6ecb7b54313b14bd50381bdb504f13d5c (patch) | |
| tree | e4ce5114be620e09b56ce41c2fa63c42c34cdcc5 /src/Cfe/Expression/Base.agda | |
| parent | a17b12baa957d7563a4240c8b46a12bf4e465423 (diff) | |
Prove satisfiability of τε.
There is a small error in the paper. It claims that L⊨τε if and only if L≈{ε}.
However, from `⊨-anticongˡ` and `≤-min`, we have ∅⊨{ε}.
Diffstat (limited to 'src/Cfe/Expression/Base.agda')
0 files changed, 0 insertions, 0 deletions