Difference between type and let?

[chandradeepdey]

Other than defining new inductive types, does type do anything let can't?

[chandradeepdey]

Ah, #3118

[nikswamy]

I tend to use type only when defining new inductive types and otherwise use let, or sometimes let t : Type = d instead of type t = d.

[chandradeepdey]

I usually do the same. Got confused when I saw something similar to #2933 working.