Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evalu

Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evaluation, it's quite uniform. > It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :) Indeed, I feel like we are just getting started finding the right "design patterns" for working with dependently typed programs. It's sort of a Wild West of styles in the Coq world currently, IMO, which is great when something is well designed but terrible when using a theorem demands you prove some clearly obvious precondition (e.g. Riemann integration in the stdlib is a pain to work with).