CakeML/cakeml

Remove mapPartial from mllist

オープン

#1,449 opened on 2026/08/12

 (0 件のコメント) (0 件のリアクション) (0 人の担当者)Standard ML (98 件のフォーク)auto 404
good first issuelow effort

Repository metrics

Stars
 (1,169 個のスター)
PR merge metrics
 (PR metrics pending)

説明

It seems that mllist redefines mapPartial which already exists in list:

listTheory.mapPartial_def;
val it =
   ⊢ (∀f. mapPartial f [] = []) ∧
     ∀f x xs.
       mapPartial f (x::xs) =
       case f x of NONE => mapPartial f xs | SOME y => y::mapPartial f xs:
   thm
> mllistTheory.mapPartial_def;
val it =
   ⊢ (∀f. mapPartial f [] = []) ∧
     ∀f h t.
       mapPartial f (h::t) =
       case f h of NONE => mapPartial f t | SOME x => x::mapPartial f t: thm

I ran into this issue after spending some time not understanding why mapPartial_def is not doing anything as I had an mllist as my ancestors.

I suspect the fix is basically as simple as just deleting the definition, with perhaps minor changes required here and there.

コントリビューターガイド