ScopedSnocList: Adapt expected

Co-authored-by: Viktor Yudov <me@spcfox.com>
idris-lang · Feb 24, 2025 · ddcf598 · ddcf598
1 parent 9a53908
commit ddcf598
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/tests/idris2/basic/basic044/expected b/tests/idris2/basic/basic044/expected
@@ -96,13 +96,13 @@ LOG declare.def:3: Initially missing in Term.NF:
 Term> Bye for now!
 1/1: Building Vec (Vec.idr)
 LOG declare.type:1: Processing Vec.Vec
-LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:1} : (Data.Fin.Fin {arg:2}[1])) -> {arg:3}[1]
+LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:1} : (Data.Fin.Fin {arg:2}[0])) -> {arg:3}[2]
 LOG declare.type:1: Processing Vec.Nil
 LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:3}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data.Fin:1)
 LOG declare.type:1: Processing Vec.(::)
-LOG declare.def:2: Case tree for Vec.(::): case {arg:4}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:3}[0])) of
+LOG declare.def:2: Case tree for Vec.(::): case {arg:4}[0] : (Data.Fin.Fin (Prelude.Types.S {arg:3}[4])) of
  { Data.Fin.FZ {e:0} => [0] {arg:5}[3]
- | Data.Fin.FS {e:1} {e:2} => [1] ({arg:6}[5] {e:2}[1])
+ | Data.Fin.FS {e:1} {e:2} => [1] ({arg:6}[3] {e:2}[0])
  }
 LOG declare.type:1: Processing Vec.test
 LOG elab.ambiguous:5: Ambiguous elaboration at Vec:1:

diff --git a/tests/idris2/data/record019/expected b/tests/idris2/data/record019/expected
@@ -11,7 +11,7 @@ LOG declare.record.parameters:50: Decided to bind the following extra parameters
   {0 ys : ((Main.Vect a) n)}
 
 LOG declare.record.parameters:60: We elaborated Main.EtaProof in a non-empty local context.
-  Dropped: [b, a]
+  Dropped: [< a, b]
   Remaining type: (p : (Main.Product a[1] b[0])) -> Type
 
 LOG declare.record.parameters:30: Unelaborated type: (%pi RigW Explicit (Just p) Main.Product %type)