good first issuelow effort
Métriques du dépôt
- Stars
- (1 169 étoiles)
- Métriques de merge PR
- (Métriques PR en attente)
Description
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.