Revert "[ fix ] Change type of localVars to SnocList Name"

This reverts commit e28870c.
idris-lang · Mar 5, 2025 · bc7f96b · bc7f96b
1 parent 24ac12f
commit bc7f96b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr
@@ -74,7 +74,7 @@ data Elab : Type -> Type where
      -- (it might need to be inferred from the solution)
      Goal : Elab (Maybe TTImp)
      -- Get the names of local variables in scope
-     LocalVars : Elab (SnocList Name)
+     LocalVars : Elab (List Name)
      -- Generate a new unique name, based on the given string
      GenSym : String -> Elab Name
      -- Put a name in the current namespace
@@ -169,7 +169,7 @@ interface Monad m => Elaboration m where
   goal : m (Maybe TTImp)
 
   ||| Get the names of the local variables in scope
-  localVars : m (SnocList Name)
+  localVars : m (List Name)
 
   ||| Generate a new unique name
   genSym : String -> m Name

diff --git a/tests/idris2/reflection/reflection006/expected b/tests/idris2/reflection/reflection006/expected
@@ -1,5 +1,5 @@
 1/1: Building refleq (refleq.idr)
-LOG 0: [< y, x]
+LOG 0: [x, y]
 LOG 0: Left: ((Prelude.Types.plus x) y)
 LOG 0: Right: ((Prelude.Types.plus y) x)
 Warning: We are about to implicitly bind the following lowercase names.