diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr index 2dee01ee6e..36c33618a1 100644 --- 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 index db2cb40c52..aeaad82c40 100644 --- 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.