|
|
|
|
|
|
by gue5t
408 days ago
|
|
|
It seems like this is grasping for languages to expose recursors[1] or induction principles. These factor out the structure of an inductive type (e.g. trees) and leave the caller to simply plug in the behavior to perform for each possible situation that might arise during traversal. [1]: https://lean-lang.org/doc/reference/latest//The-Type-System/... |
|
|