diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-08 17:17:04 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-08 17:17:04 +0100 |
| commit | d5794f15b40ef4c683d713ffad027e94f2caf17e (patch) | |
| tree | 45471d492da2da49243d158952b10282d0cf0322 /src/Total/LogRel.idr | |
| parent | c64650ee0f41a1ebe45cf92c9b999f39825e9f5e (diff) | |
Use CoDebruijn syntax at top level.
Diffstat (limited to 'src/Total/LogRel.idr')
| -rw-r--r-- | src/Total/LogRel.idr | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/Total/LogRel.idr b/src/Total/LogRel.idr index ebde8d5..90bec66 100644 --- a/src/Total/LogRel.idr +++ b/src/Total/LogRel.idr @@ -181,19 +181,18 @@ allValid help (Abs t) sub allRels = (let rec = valid - (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here) - (wknAllRel help allRels (Drop $ id @{termsLen sub}) :< help.var Here) + (wknAll sub (Drop id) :< Var Here) + (wknAllRel help allRels (Drop id) :< help.var Here) in help.abs rec , \thin, u, rel => let eq : (subst - (wkn (subst t (wknAll sub (Drop $ id @{termsLen sub}) :< Var Here)) (Keep thin)) - (Base (id @{length _}) :< u) = + (wkn (subst t (wknAll sub (Drop Thinning.id) :< Var Here)) (Keep thin)) + (Base Thinning.id :< u) = subst t (wknAll sub thin :< u)) eq = - rewrite lenUnique (termsLen sub) (length ctx') in Calc $ |~ subst (wkn (subst t (wknAll sub (Drop id) :< Var Here)) (Keep thin)) (Base id :< u) ~~ subst (subst t (wknAll sub (Drop id) :< Var Here)) (restrict (Base id :< u) (Keep thin)) @@ -219,8 +218,8 @@ allValid help (Abs t) sub allRels = allValid help (App t u) sub allRels = let (pt, app) = allValid help t sub allRels in let rel = allValid help u sub allRels in - rewrite sym $ wknId @{termsLen sub} (subst t sub) in - app (id @{termsLen sub}) (subst u sub) rel + rewrite sym $ wknId (subst t sub) in + app id (subst u sub) rel allValid help Zero sub allRels = help.zero allValid help (Suc t) sub allRels = let pt = allValid help t sub allRels in @@ -240,4 +239,4 @@ allRel : (t : Term ctx ty) -> P t allRel help t = - rewrite sym $ substId @{length ctx} t in escape (allValid help t (Base $ id @{length ctx}) Base) + rewrite sym $ substId t in escape (allValid help t (Base id) Base) |