rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add CanSubst Var (Term/Elim)

Browse source
This commit is contained in:
rhiannon morris 2021-09-09 23:55:30 +02:00
parent 8c675d01d5
commit 4a2f7e1497
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Quox/Syntax/Term.idr
View file

@ -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)}