rachel
/
pi
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

remove unneeded weaken function (which was wrong anyway)

master
Rachel Lambda Samuelsson 2022-05-13 19:48:20 +02:00
parent 40b089be6e
commit dea31b675d
1 changed files with 0 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
src/Term.idr
View File

@ -25,44 +25,3 @@ Show (Term n) where
show (TPi ty sc) = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
show (TApp f x) = "TApp (" ++ show f ++ ") (" ++ show x ++ ")"
show (TVar i _) = "TVar " ++ show i
public export
weaken : {p, q : _} -> LTE p q -> Term p -> Term q
weaken _ TType = TType
weaken p (TLam sc) = TLam (weaken (LTESucc p) sc)
weaken p (TPi a bx) = TPi (weaken p a) (weaken (LTESucc p) bx)
weaken p (TApp f x) = TApp (weaken p f) (weaken p x)
{-
Getting new index
=================
New index is
old + Δctx
in this case
r + (q - p)
which since p <= q is equivalent to
(r + q) - p
Proving validity of new index
=============================
r < p => (+mono)
r + q < p + q => (-mono)
(r + q) - p < (p + q) - p => (lteTransp -+)
(r + q) - p < q ∎
-}
weaken {p = S p} {q = S q} (LTESucc p1) (TVar r p2' ) =
case p2' of
LTESucc p2 => TVar (minus (r + q) p)
(LTESucc (lteTransp (minusLteMonotone (plusLteMonotoneRight q r p p2)) Refl (minusPlus p)))
weaken1 : {n : _} -> Term n -> Term (S n)
weaken1 = weaken lteS