diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-11 16:25:24 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-11 16:25:24 +0100 |
| commit | 60df32ffd5b88498e4634649509bbd0810421004 (patch) | |
| tree | 646cf040522eb217ff3188e4b9b68b170e539f0b /src/Data/Term/Zipper.idr | |
| parent | 60d5896ab7939ae42cf7744f93e8eaefa0675854 (diff) | |
Begin big unification proof.
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 |