Great, thanks again! One more question: I imagine that it's not very important exactly what one picks as a beginner, but is Lean something which one might weigh

Great, thanks again! One more question: I imagine that it's not very important exactly what one picks as a beginner, but is Lean something which one might weight against Idris as something to start with, or would one get very different things out of learning about (and how to use) those?