diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr index f05f64e..6dd0e90 100644 --- a/src/Quox/Syntax/Dim.idr +++ b/src/Quox/Syntax/Dim.idr @@ -61,6 +61,11 @@ prettyDSubst th = export FromVar Dim where fromVar = B +export +CanShift Dim where + K e // _ = K e + B i // by = B (i // by) + export CanSubst Dim Dim where K e // _ = K e