From 0d3bb6213f086d03a82debaa79f7ff049fb3330d Mon Sep 17 00:00:00 2001
From: "Serge S. Gulin" <gulin.serge@gmail.com>
Date: Fri, 16 Aug 2024 00:50:45 +0300
Subject: [PATCH] ScopedSnocList: special operators for snoc simulation

---
 src/Core/Name/ScopedList.idr | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/Core/Name/ScopedList.idr b/src/Core/Name/ScopedList.idr
index 2f9f1f7215..06170e609e 100644
--- a/src/Core/Name/ScopedList.idr
+++ b/src/Core/Name/ScopedList.idr
@@ -18,7 +18,12 @@ mutual
   data ScopedList a = Lin | (:%:) a (ScopedList a)
   -- TODO: make that a SnocList
 
-export infixr 7 +%+
+export infixl 7 :<%:
+
+public export
+(:<%:) : ScopedList as -> as -> ScopedList as
+(:<%:) [<] a = a :%: [<]
+(:<%:) as a = a :%: as
 
 public export
 length : ScopedList a -> Nat
@@ -65,6 +70,8 @@ Zippable ScopedList where
                                 (bs, cs, ds) = unzipWith3 f xs in
                                 (b :%: bs, c :%: cs, d :%: ds)
 
+export infixr 7 +%+
+
 public export
 (+%+) : (xs, ys : ScopedList a) -> ScopedList a
 (+%+) [<] ys = ys
@@ -263,6 +270,12 @@ public export
 reverse : ScopedList a -> ScopedList a
 reverse = reverseOnto [<]
 
+export infixl 7 +<%+
+
+public export
+(+<%+) : (xs, ys : ScopedList a) -> ScopedList a
+(+<%+) xs ys = ys +%+ xs
+
 hasLengthReverseOnto : HasLength m acc -> HasLength n xs -> HasLength (m + n) (reverseOnto acc xs)
 hasLengthReverseOnto p Z = rewrite plusZeroRightNeutral m in p
 hasLengthReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hasLengthReverseOnto (S p) q