From 6a2ca507f4f1de892182dbb62a8fee6a89428aa5 Mon Sep 17 00:00:00 2001 From: "Serge S. Gulin" Date: Mon, 23 Sep 2024 11:59:04 +0300 Subject: [PATCH] ScopedSnocList: WIP: `a (b +%+ c) => a (c ++ b)` but actually a special case for `elemInsertedMiddle` --- src/Core/Case/CaseBuilder.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr index d42fabdc09..fc4b42ee3a 100644 --- a/src/Core/Case/CaseBuilder.idr +++ b/src/Core/Case/CaseBuilder.idr @@ -688,7 +688,7 @@ zeroedScore nps = Scored nps (replicate (S $ length ps) 0) ||| Proof that a value `v` inserted in the middle of a list with ||| prefix `ps` and suffix `qs` can equivalently be snoced with ||| `ps` or consed with `qs` before appending `qs` to `ps`. -elemInsertedMiddle : (v : a) -> (ps,qs : SnocList a) -> (ps +%+ (qs :< v)) = ((ps `snoc` v) +%+ qs) +elemInsertedMiddle : (v : a) -> (ps,qs : SnocList a) -> ((qs :< v) ++ ps) = (qs ++ (ps `snoc` v)) elemInsertedMiddle v [<] qs = Refl elemInsertedMiddle v (xs :< x) qs = rewrite elemInsertedMiddle v xs qs in Refl