diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-05-24 14:21:53 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-05-24 14:38:26 +0100 |
| commit | 2aa256f4c60caa57a641ecf0962db0f69cab455a (patch) | |
| tree | f990f24538271d4696067089db8999f5f5928faf /src/Term.idr | |
| parent | 1207476a583ee527d78c3ff43e8a6757ea3406c4 (diff) | |
Make normal forms a property.
Weakening is now part of eval.
Diffstat (limited to 'src/Term.idr')
| -rw-r--r-- | src/Term.idr | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Term.idr b/src/Term.idr index e6cf25c..fde8d9f 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -46,18 +46,20 @@ lift : Subst ctx ctx' -> Subst (ctx :< ty) (ctx' :< ty) lift (Base thin) = Base (keep thin) lift (sub :< t) = shift (sub :< t) :< Var Here -export +public export index : Subst ctx' ctx -> Elem ty ctx -> Term ctx' ty index (Base thin) i = Var (index thin i) index (sub :< t) Here = t index (sub :< t) (There i) = index sub i +public export restrict : Subst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> Subst ctx1 ctx3 restrict (Base thin') thin = Base (thin' . thin) restrict (sub :< t) Id = sub :< t restrict (sub :< t) (Drop thin) = restrict sub thin restrict (sub :< t) (Keep thin) = restrict sub thin :< t +export (.) : Subst ctx1 ctx2 -> Subst ctx2 ctx3 -> Subst ctx1 ctx3 sub2 . Base thin = restrict sub2 thin sub2 . (sub1 :< t) = sub2 . sub1 :< Sub t sub2 |