Dafnyで部分範囲型を宣言したら、C#のどういうコードにトランスパイルされるんだろう？＞＜　と思って
"""
type NumMonth = x: int | 1 <= x <= 12 witness 1
"""
とだけ書いたコードでやってみたら、5708行、242.97KiBのC# のコードが生成されて、宇宙猫みたいになった＞＜；