ScopedSnocList: WIP: add import Libraries.Data.SnocList.SizeOf and …

…`import Core.Name.CompatibleVars`
idris-lang · Sep 27, 2024 · 9ac2b79 · 9ac2b79
1 parent ef3e395
commit 9ac2b79
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 0 deletions.
diff --git a/src/Core/TT/Subst.idr b/src/Core/TT/Subst.idr
@@ -6,6 +6,8 @@ import Core.TT.Var
 
 import Data.SnocList
 
+import Libraries.Data.SnocList.SizeOf
+
 %default total
 
 public export

diff --git a/src/Core/TT/Term.idr b/src/Core/TT/Term.idr
@@ -6,13 +6,16 @@ import Core.FC
 
 import Core.Name
 import Core.Name.Scoped
+import Core.Name.CompatibleVars
 import Core.TT.Binder
 import Core.TT.Primitive
 import Core.TT.Var
 
 import Data.List
 import Data.SnocList
 
+import Libraries.Data.SnocList.SizeOf
+
 %default total
 
 ------------------------------------------------------------------------

diff --git a/src/Core/TT/Term/Subst.idr b/src/Core/TT/Term/Subst.idr
@@ -10,6 +10,8 @@ import Core.TT.Var
 
 import Data.SnocList
 
+import Libraries.Data.SnocList.SizeOf
+
 %default total
 
 public export