ScopedSnocList: WIP: aligned with Yaffle the following: Context.

idris-lang · Oct 1, 2024 · a14a3bf · a14a3bf
1 parent d7b8fb2
commit a14a3bf
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
@@ -556,13 +556,13 @@ mutual
 
 export
 HasNames (Env Term vars) where
-  full gam [] = pure []
-  full gam (b :: bs)
-      = pure $ !(traverse (full gam) b) :: !(full gam bs)
+  full gam [<] = pure [<]
+  full gam (bs :< b)
+      = pure $ !(full gam bs) :< !(traverse (full gam) b)
 
-  resolved gam [] = pure []
-  resolved gam (b :: bs)
-      = pure $ !(traverse (resolved gam) b) :: !(resolved gam bs)
+  resolved gam [<] = pure [<]
+  resolved gam (bs :< b)
+      = pure $ !(resolved gam bs) :< !(traverse (resolved gam) b)
 
 export
 HasNames Clause where