I've been defining notions of finiteness of trees here and there several time by now, so it's more than time to just push some theory around it in the library.
This PR defines a "box" and a "diamond" predicate expressing whether we mean always finite or the existence of a finite branch. Elementary theory for both is provided, as well as their relationship to the [Image] predicate from PR#211.
Notably, I currently do not provide any theory related to [iter] in this PR, it should be coming relatively soon.
I stored this file in Core, let me know if anyone thinks there's a better place. More generally, any complaints or requests before merge are welcome!
Hey everyone,
I've been defining notions of finiteness of trees here and there several time by now, so it's more than time to just push some theory around it in the library.
This PR defines a "box" and a "diamond" predicate expressing whether we mean always finite or the existence of a finite branch. Elementary theory for both is provided, as well as their relationship to the [Image] predicate from PR#211.
Notably, I currently do not provide any theory related to [iter] in this PR, it should be coming relatively soon.
I stored this file in
Core, let me know if anyone thinks there's a better place. More generally, any complaints or requests before merge are welcome!Best, Yannick