From 4a2f7e1497042c88559bbfecd04b5aeaea1a3c15 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 9 Sep 2021 23:55:30 +0200 Subject: [PATCH] add CanSubst Var (Term/Elim) --- src/Quox/Syntax/Term.idr | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr index e5bba64..38dc637 100644 --- a/src/Quox/Syntax/Term.idr +++ b/src/Quox/Syntax/Term.idr @@ -209,6 +209,9 @@ CanSubst (Elim d) (Term d) where Shift SZ => s th => CloT s th +export CanSubst Var (Term d) where s // th = s // map (B {d}) th +export CanSubst Var (Elim d) where e // th = e // map (B {d}) th + export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)} export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}