ScopedSnocList: special operators for snoc simulation

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