Compare commits

..

No commits in common. "068d0218b0fbbbfc6cd200fd0c268b9cdab1e15f" and "7623787b1cbb16e73ba5caf326bbe40ac50855a7" have entirely different histories.

2 changed files with 1 additions and 5 deletions

View File

@ -361,7 +361,7 @@ I think this is a good approach. Should we want to add more types to our languag
lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality
proofs, and keep the `typecheck` method the same. Had we not used this approach,
and instead decided to pattern match on types inside of `typecheck`, we would've quickly
found that this only works for languages with finitely many types. When we add polymorphic tuples
found that this only works for types with finitely many values. When we add polymorphic tuples
and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive
solution. I think that this leads us back to `decEq`.

View File

@ -54,10 +54,6 @@ div.highlight table {
code {
border: none;
}
span {
margin: 0 !important;
}
}
.container {