top | item 43838221

(no title)

gue5t | 10 months 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/...

discuss

order

No comments yet.