cv_trans fails with "non-cv constant" on MEM with constructor list

[xrchz]

(Generated with Claude Code)

When using cv_trans on a definition containing MEM x [Constructor1; Constructor2; ...], the translation fails with:

Exception: Encountered non-cv constant: Mod

Minimal example:

Given a datatype with constructors and a definition like:

  Definition supported_arith_def[simp]:
    (supported_arith a IntT =
       if MEM a [Add; Sub; Mul; Div; Mod] then SOME (2:num) else NONE) ∧
    (supported_arith a Float64T =
       if MEM a [Abs; Neg; Sqrt] then SOME 1 else
       if MEM a [Add; Sub; Mul; Div] then SOME 2 else
       if a = FMA then SOME 3 else NONE) ∧
    (supported_arith _ _ = NONE)
  End

Running:
cv_trans supported_arith_def

Fails with the error about Mod (or whichever constructor appears in the list).

Workaround:

Applying SRULE [] before cv_trans works around the issue by simplifying the MEM expressions:

  cv_trans (SRULE [] supported_arith_def)

Expected behavior:

cv_trans should either:

1. Automatically simplify MEM x [c1; c2; ...] into disjunctions (x = c1) ∨ (x = c2) ∨ ... before translation, or
2. Properly handle the MEM with a list of constructors

Context:

Encountered in CakeML regression testing (job 3089) when translating type inference code after adding new arithmetic operators.

[tanyongkiam]

This is a HOL issue

[xrchz]

True - my mistake. @myreen do you want me to make one there instead and link to this?

[myreen]

True - my mistake. @myreen do you want me to make one there instead and link to this?

Here is fine