Compare commits
	
		
			No commits in common. "068d0218b0fbbbfc6cd200fd0c268b9cdab1e15f" and "7623787b1cbb16e73ba5caf326bbe40ac50855a7" have entirely different histories.
		
	
	
		
			068d0218b0
			...
			7623787b1c
		
	
		
| @ -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 | 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, | 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 | 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 | 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 | 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`. | solution. I think that this leads us back to `decEq`. | ||||||
|  | |||||||
| @ -54,10 +54,6 @@ div.highlight table { | |||||||
|     code { |     code { | ||||||
|         border: none; |         border: none; | ||||||
|     } |     } | ||||||
| 
 |  | ||||||
|     span { |  | ||||||
|         margin: 0 !important; |  | ||||||
|     } |  | ||||||
| } | } | ||||||
| 
 | 
 | ||||||
| .container { | .container { | ||||||
|  | |||||||
		Loading…
	
		Reference in New Issue
	
	Block a user