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.