模式只有三种,lemma 体的取舍

模式只有三种

同一条规则，不是两条。_ 是"匹配任何东西、但我不打算用它"，出现在哪个位置都是这个意思。

在 Cons(_, tl) 里，它站在构造子的参数位上，吃掉头。在 case _ => 0 里，它站在整个被匹配值的位置上，吃掉 m 本身。位置不同，语义一样：占位、不命名。

再往前推一步：你之前写的 case default 也是这个逻辑。

Cons(hd, tl) 里的 hd 是绑定变量，case default 里的 default 也是绑定变量。

所以 Dafny 的模式其实只有三种：字面量或构造子（要求相等）、标识符（绑定）、下划线（绑定但丢弃）。

你把它们记成"Cons 专用"和"default 专用"，是在给一条规则贴两个标签，考试时容易在陌生位置上卡住。

daysInMonth（dates-with-months.dfy）

function daysInMonth(m : nat, isLeapYear : bool) : nat
{
    match m {
        case 1 | 3 | 5 | 7 | 8 | 10 | 12 => 31
        case 2 => if isLeapYear then 29 else 28
        case 4 | 6 | 9 | 11 => 30
        case _ => 0
    }
}

lemma daysInMonthOutputOK(m:nat, isLeapYear:bool)

lemma 体的取舍

lemma体什么时候写、什么时候留空，标准只有一个——空体先跑一遍，过了就不加。