lamda_calculus_formalizations VS lambda-calculus-hs

This is really cool. I've been doing something in a similar vein at https://github.com/sgodwincs/lamda_calculus_formalizations, though the difference being I'm using Lean and trying to prove certain properties of the languages (type safety, normalization, etc.). Of course, compared to unification and stuff you have, I only have very simple additions like natural numbers and binary product types (though the proofs still are hard for me!). Working on finite product types now and it's an absolute pain to even define it in a way that Lean likes.

I've noticed amongst many peers that when going down the type theory/pl theory journey there is a ton of hidden knowledge and context we all find ourselves collecting.

All of this knowledge and context spread amongst a common set of books, papers, blog posts, and git repos floating around the internet.

At the risk of creating yet another partial silo, I decided earlier this year to create a project similar to the [Elaboration Zoo](https://github.com/AndrasKovacs/elaboration-zoo) but focused on a blessed path to MLTT with a number of the desirable language features via bidirectional typechecking.

https://github.com/solomon-b/lambda-calculus-hs

The project is incomplete and my end goal is a website like the [1 Lab](https://1lab.dev) but focused on Type Theory and PL Theory, but I ran low on steam and could use some collaborators.