From ec634f06a33acf7dac401a61701a0039beb9274a Mon Sep 17 00:00:00 2001 From: Zachary Kent Date: Thu, 21 May 2026 22:00:44 +0000 Subject: [PATCH] fix: add FStar.Mul compat shim for nightly-2026-04-29 FStar.Mul was removed and op_Multiply renamed to op_Star in this nightly. Add a shim that re-exports op_Multiply using the new infix operator, and add missing imports to two files that used op_Multiply without opening FStar.Mul. Closes #8 --- ismm/FStar.Mul.fst | 6 ++++++ ismm/ISMM.UF.SizeRank.fst | 1 + ismm/ISMM.UnionFind.Spec.fst | 1 + 3 files changed, 8 insertions(+) create mode 100644 ismm/FStar.Mul.fst diff --git a/ismm/FStar.Mul.fst b/ismm/FStar.Mul.fst new file mode 100644 index 00000000..368e7121 --- /dev/null +++ b/ismm/FStar.Mul.fst @@ -0,0 +1,6 @@ +module FStar.Mul + +// Compatibility shim: FStar.Mul was removed in F* nightly-2026-04-29. +// The multiplication operator is now op_Star rather than op_Multiply. + +let op_Multiply (x y: int) : int = x * y diff --git a/ismm/ISMM.UF.SizeRank.fst b/ismm/ISMM.UF.SizeRank.fst index 4709a9bf..d1ebd55f 100644 --- a/ismm/ISMM.UF.SizeRank.fst +++ b/ismm/ISMM.UF.SizeRank.fst @@ -8,6 +8,7 @@ module ISMM.UF.SizeRank open FStar.Seq +open FStar.Mul module Seq = FStar.Seq open ISMM.UnionFind.Spec diff --git a/ismm/ISMM.UnionFind.Spec.fst b/ismm/ISMM.UnionFind.Spec.fst index 32c6c8af..eb2b3730 100644 --- a/ismm/ISMM.UnionFind.Spec.fst +++ b/ismm/ISMM.UnionFind.Spec.fst @@ -17,6 +17,7 @@ module ISMM.UnionFind.Spec open FStar.Seq +open FStar.Mul module Seq = FStar.Seq open ISMM.Status