diff options
Diffstat (limited to 'src/Total/Reduction.idr')
| -rw-r--r-- | src/Total/Reduction.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr index 4870f30..cb13706 100644 --- a/src/Total/Reduction.idr +++ b/src/Total/Reduction.idr @@ -95,3 +95,8 @@ wknStep (RecCong2 step) = RecCong2 (wknStep step) wknStep (RecCong3 step) = RecCong3 (wknStep step) wknStep RecZero = RecZero wknStep RecSuc = RecSuc + +export +wknSteps : t >= u -> wkn t thin >= wkn u thin +wknSteps [<] = [<] +wknSteps (steps :< step) = wknSteps steps :< wknStep step |