OPE & scope stuff

This commit is contained in:
rhiannon morris 2022-10-10 17:30:46 +02:00
parent 23c008b57a
commit 53bbcbf8c7
2 changed files with 4 additions and 0 deletions

View file

@ -116,6 +116,7 @@ pushSubstsE' : Elim d n -> Elim d n
pushSubstsE' e = (pushSubstsE e).fst
{- [todo] remove these probably?
mutual
-- tightening a term/elim also causes substitutions to be pushed through.
-- this is because otherwise a variable in an unused part of the subst
@ -156,6 +157,7 @@ mutual
Tighten (ScopeTerm d) where
tighten p (TUsed body) = TUsed <$> tighten (Keep p) body
tighten p (TUnused body) = TUnused <$> tighten p body
-}
public export %inline

View file

@ -264,6 +264,7 @@ decEqFromBool i j =
public export %inline DecEq (Var n) where decEq = varDecEq
{- [todo] remove this probably?
export
Tighten Var where
tighten Id i = pure i
@ -271,3 +272,4 @@ Tighten Var where
tighten (Drop q) (VS i) = tighten q i
tighten (Keep q) VZ = pure VZ
tighten (Keep q) (VS i) = VS <$> tighten q i
-}