From 3f5c7807f39202a1a2ecb52198031e5846cfb54a Mon Sep 17 00:00:00 2001
From: Your Name <you@example.com>
Date: Mon, 22 Sep 2025 11:48:42 +0200
Subject: [PATCH] =?UTF-8?q?feat:=20=C3=9Cbersetze=20Isabelle-Datentyp=20Ag?=
 =?UTF-8?q?ent=20nach=20Lean4=20als=20induktiven=20Typ?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: aider (gpt-4o) <aider@aider.chat>
---
 InductiveVerification.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/InductiveVerification.lean b/InductiveVerification.lean
index d9843f5..c076509 100644
--- a/InductiveVerification.lean
+++ b/InductiveVerification.lean
@@ -1,3 +1,8 @@
 -- This module serves as the root of the `InductiveVerification` library.
 -- Import modules here that should be built as part of the library.
 import InductiveVerification.Basic
+
+inductive Agent
+  | Server : Agent
+  | Friend : Nat → Agent
+  | Spy : Agent