michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

547 - Proving trans using ≡-Reasoning is circular

Browse source
This commit is contained in:
Cristóvão Gomes Ferreira (Melo Gibson) 2020-12-03 20:14:48 +00:00
parent 8c9782d9b6
commit 40b63478ba
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/plfa/part1/Equality.lagda.md
View file

@ -268,6 +268,14 @@ simplifies to a chain of applications of `trans` that ends in `trans e
refl`, where `e` is a term that proves some equality, even though `e` refl`, where `e` is a term that proves some equality, even though `e`
alone would do. alone would do.
#### Exercise `trans` and `≡-Reasoning` (practice)
Sadly, we cannot use the definition of trans' using ≡-Reasoning as the definition
for trans. Can you see why? (Hint: look at the definition of `_≡⟨_⟩_`)
```
-- Your code goes here
```
## Chains of equations, another example ## Chains of equations, another example