From f9206e29e51b148d9acb18206312531670a17164 Mon Sep 17 00:00:00 2001 From: Guillaume Allais <guillaume.allais@ens-lyon.org> Date: Tue, 28 Nov 2023 17:26:29 +0000 Subject: [PATCH] [ cleanup ] remove unused unsafe definition --- src/Core/Name/Scoped.idr | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/Core/Name/Scoped.idr b/src/Core/Name/Scoped.idr index 0e09d83c62..69169b3435 100644 --- 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?