[ cleanup ] remove unused unsafe definition

idris-lang · Nov 28, 2023 · f9206e2 · f9206e2
1 parent 9f6ffc9
commit f9206e2
Showing 1 changed file with 0 additions and 7 deletions.
diff --git a/src/Core/Name/Scoped.idr b/src/Core/Name/Scoped.idr
@@ -119,13 +119,6 @@ keeps : (args : List a) -> Thin xs ys -> Thin (args ++ xs) (args ++ ys)
 keeps [] th = th
 keeps (x :: xs) th = keep (keeps xs th)
 
-namespace Thin
-  -- At runtime, Thin's `Refl` does not carry any additional
-  -- information. So this is safe!
-  export
-  embed : Thin xs ys -> Thin (xs ++ outer) (ys ++ outer)
-  embed = believe_me
-
 ||| Compute the thinning getting rid of the listed de Bruijn indices.
 -- TODO: is the list of erased arguments guaranteed to be sorted?
 -- Should it?