From c290706fed69d622cfe988e732e1ad01d09e569d Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Sun, 8 Mar 2026 18:26:33 +0100
Subject: rework file structure

---
 lib/Wayland/Basic/Lens.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 lib/Wayland/Basic/Lens.lean

(limited to 'lib/Wayland/Basic/Lens.lean')

diff --git a/lib/Wayland/Basic/Lens.lean b/lib/Wayland/Basic/Lens.lean
new file mode 100644
index 0000000..16de458
--- /dev/null
+++ b/lib/Wayland/Basic/Lens.lean
@@ -0,0 +1,22 @@
+/-!
+# Lenses
+
+A `Lens` bundles a getter and an (updating) setter which can be used to elegantly describe a field of a structure.
+-/
+
+namespace Wayland
+
+/-- A lens that points into a substructure of type `I` within a structure of type `O`. -/
+structure Lens (O I : Type) where
+  /-- Get the substructure from the outer structure. -/
+  get : O → I
+  /-- Update the outer structure to contain the updated substructure. -/
+  set : I → O → O
+
+/-- 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 #[]]
+  let lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal := ⟨lvalNode⟩
+  `({ get := fun x => x.$field, set := fun i x => { x with $lval := i } })
+
+end Wayland
-- 
cgit v1.3.1