lens composition

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/Wayland/Basic/Lens.lean b/lib/Wayland/Basic/Lens.lean
index 16de458..ee1e486 100644
--- a/lib/Wayland/Basic/Lens.lean
+++ b/lib/Wayland/Basic/Lens.lean
@@ -13,6 +13,16 @@ structure Lens (O I : Type) where
   /-- Update the outer structure to contain the updated substructure. -/
   set : I → O → O
 
+def Lens.id (X : Type) : Lens X X where
+  get x := x
+  set x _ := x
+
+def Lens.compose {X Y Z : Type} (l₁ : Lens X Y) (l₂ : Lens Y Z) : Lens X Z where
+  get := l₂.get ∘ l₁.get
+  set i o := l₁.set (l₂.set i (l₁.get o)) o
+
+scoped infixr:80 " ≫ " => Lens.compose
+
 /-- Helper for writing a `Lens` constructor for a named field of a structure. -/
 macro "mk_lens " field:ident : term => do
   let lvalNode := Lean.mkNode `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode #[]]