I am not aware of a formal comparison, but I would assume that one can construct a model of the dependent type theory of Lean in set theory, and thus in TLA+. It could make for a nice research project to make this precise. In practice, both languages are of course highly expressive.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5736505E-EE27-4422-A8F4-23D73354E2E7%40gmail.com.