See the Coq proofs in https://github.com/barry-jay-personal/tree-calculus/ for the pre-typed tree content as well.
HN user
justosophy
Tree Calculus is awesome with implications beyond this website.
Shame the website doesn't attribute the creator and author Prof. Barry Jay. (Seems to be a pattern for them sadly, not sure why)
See Jay's book on GitHub for more https://github.com/barry-jay-personal/tree-calculus/blob/mas...
Good to see more attention to this. AWS did a presentation on it last year.
Some simplified exercises of isomorphic equivalence in data structures.
Haskell experts may now commence their superior mocking ;)
Tipping isn't a thing in Australia. I'm not sure I'd know the first thing for the right way to tip if I visited the US. And yet we seem to enjoy high quality food, and I believe our hospitality wages are higher in general.
( perhaps this is all anecdotal, but tipping has never seemed to make sense to someone not in the mix of it )