diff options
Diffstat (limited to 'src/Data/Term/Zipper.idr')
| -rw-r--r-- | src/Data/Term/Zipper.idr | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr index 608e86c..ddc0797 100644 --- a/src/Data/Term/Zipper.idr +++ b/src/Data/Term/Zipper.idr @@ -115,6 +115,10 @@ actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $ ~~ insertAt' i (f <$> zip + t) (map (f <$>) ts) ...(mapInsertAt (f <$>) i (zip + t) ts) ~~ insertAt' i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt' i t (map (f <$>) ts)) $ actionHomo f zip t) +export +invertActionTop : (zip : Zipper sig k) -> (0 _ : f <$> zip = Top) -> zip = Top +invertActionTop Top prf = Refl + -- Cycles ---------------------------------------------------------------------- pivotAt : sig.Operator k -> SFin k -> Vect k (Term sig n) -> Zipper sig n |