Tweaks

tools/src/extract.ts

@@ -1880,7 +1880,8 @@ export function extractModule(sourceFile: SourceFile): RawModule {
       const name = recordMatch[1];
       // `<T extends B>` → bare `T`: a Dafny type param, like the def path.
       const typeParams = recordMatch[2]?.split(",").map(s => s.trim().split(/\s+extends\s+/)[0].trim()).filter(Boolean);
-      const fields = recordMatch[3].split(",").map(f => f.trim()).filter(Boolean).map(f => {
+      // Split on `,` OR `;` — TS object types allow both.
+      const fields = recordMatch[3].split(/[,;]/).map(f => f.trim()).filter(Boolean).map(f => {
         const [fname, ftype] = f.split(":").map(s => s.trim());
         const synth = _synthFromTsTypeString(ftype);
         return { name: fname, tsType: synth ?? ftype };

tools/src/transform.ts

@@ -602,6 +602,13 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
           else: { kind: "var", name: "undefined" },
         };
       }
+      // || on a number → `if x != 0 then x else default` (0 the only falsy int).
+      if (e.op === "||" && (e.left.ty.kind === "int" || e.left.ty.kind === "nat")) {
+        const left = lowerExpr(e.left, binds);
+        const right = lowerExpr(e.right, binds);
+        const truthy = valueTruthyCond(left, e.left.ty)!;
+        return { kind: "if", cond: truthy, then: left, else: right };
+      }
       // String concatenation: `+` with a string operand. Stringify int/nat
       // operands (Dafny NatToString, Lean toString) and join with arrayConcat
       // (rendered `+` in Dafny, `++` in Lean).