|
|
|
|
|
|
by gugagore
357 days ago
|
|
|
Right, though the embedding is trivial, the conceptual distinction is not. In Lean, a subtype is a refinement that restricts by proof. In OOP, a subclass augments or overrides behavior. It's composition versus inheritance. The trivial embedding masks a fundamental shift in what "subtype" means. |
|
|