CakeML/cakeml

Remove mapPartial from mllist

開放

#1,449 建立於 2026年8月12日

 (0 則留言) (0 個反應) (0 位負責人)Standard ML (98 個分叉)auto 404
good first issuelow effort

倉庫指標

星標
 (1,169 顆星)
PR 合併指標
 (PR 指標待抓取)

描述

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.

貢獻者指南