6260 Notes: Happy Dafny

6260 notes: setlists,member,subset_union,subset_trans

12 minute read Published: 2026-08-31

6260 notes: setlists,member_union,函数调用≠lemma调用

3 minute read Published: 2026-08-31

6260 notes: case split,账目表,展开一次一层,subset_widen

6 minute read Published: 2026-08-31

6260 notes: 词典序度量、互递归、终止性与第一份归纳证明

12 minute read Published: 2026-08-31

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

2 minute read Published: 2026-08-30