From 60e78ddc0757f58917b3d95389dd54f64f109feb Mon Sep 17 00:00:00 2001 From: "Serge S. Gulin" Date: Mon, 23 Sep 2024 11:55:02 +0300 Subject: [PATCH] ScopedSnocList: WIP: `$AA +%+ ($BB <>> ($CC +%+ $DD)) => ($BB <>> ($DD ++ $CC)) ++ $AA` --- src/Core/TT.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Core/TT.idr b/src/Core/TT.idr index b916c74b04..432acd3f3f 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -402,7 +402,7 @@ export resolveRef : SizeOf outer -> SizeOf done -> Bounds bound -> FC -> Name -> - Maybe (Var (outer +%+ (done <>> (bound +%+ vars)))) + Maybe (Var ((done <>> (vars ++ bound)) ++ outer)) resolveRef _ _ None _ _ = Nothing resolveRef {outer} {vars} {done} p q (Add {xs} new old bs) fc n = if n == old