rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

remove unused Tighten impl

Browse source
This commit is contained in:
rhiannon morris 2023-07-17 18:10:13 +02:00
parent 3c0989dcb2
commit 349cf2f477
1 changed files with 0 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
lib/Quox/Syntax/Term/Tighten.idr
View file

@ -8,23 +8,11 @@ import Quox.No
%default total %default total
export
Tighten (Shift f) where
-- `OPE m n` is a spicy `m ≤ n`,
-- and `Shift f n` is a (different) spicy `f ≤ n`
-- so the value is `f ≤ m` (as a `Shift`), if that is the case
tighten _ SZ = Nothing
tighten Id by = Just by
tighten (Drop p) (SS by) = tighten p by
tighten (Keep p) (SS by) = [|SS $ tighten p by|]
export export
Tighten Dim where Tighten Dim where
tighten p (K e loc) = pure $ K e loc tighten p (K e loc) = pure $ K e loc
tighten p (B i loc) = B <$> tighten p i <*> pure loc tighten p (B i loc) = B <$> tighten p i <*> pure loc
export export
tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) -> tightenScope : (forall m, n. OPE m n -> f n -> Maybe (f m)) ->
{s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m) {s : Nat} -> OPE m n -> Scoped s f n -> Maybe (Scoped s f m)