mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-03 18:27:13 +03:00
fix typo in equality docs
This commit is contained in:
parent
2764c4c17d
commit
d84640201d
@ -69,7 +69,7 @@ A <> B ::=
|
||||
check if A and B are "textually" the same
|
||||
```
|
||||
|
||||
So, for example, to check if `(pair 1 2) == (pair 1 (+ 2 2))`, we would first
|
||||
So, for example, to check if `(pair 1 4) == (pair 1 (+ 2 2))`, we would first
|
||||
check of both sides are identical. They're not, as evidenced by the fact they
|
||||
have different writings. We then reduce A and B to weak normal, and check if
|
||||
they're similar. This will recursivelly check if `1 == 1` and `4 == (+ 2 2)`.
|
||||
|
Loading…
Reference in New Issue
Block a user