You are answering a question you want to answer, not the one I asked! :) Yes, dependent types can encode nice constraints, but so can asserts and assumes. I a

You are answering a question you want to answer, not the one I asked! :) Yes, dependent types can encode nice constraints, but so can asserts and assumes. I am not seeing the fundamental difference in yeeting these constraints to a solver. Dafny seems to do the same thing with Z3.