From b5dd9dd4fe24a3687937b5bd5e5a892614e30a66 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Mon, 10 Jul 2023 12:53:04 -0500
Subject: [PATCH] Add test for issue #4269

---
 Source/DafnyPipeline.Test/FormatterIssues.cs | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs
index 73549f96ec2..9e94b90b17f 100644
--- a/Source/DafnyPipeline.Test/FormatterIssues.cs
+++ b/Source/DafnyPipeline.Test/FormatterIssues.cs
@@ -7,6 +7,26 @@ namespace DafnyPipeline.Test;
 [Collection("Singleton Test Collection - FormatterForTopLevelDeclarations")]
 public class FormatterIssues : FormatterBaseTest {
   [Fact]
+    public void GitIssue4269FormatLemmaIde() {
+      FormatterWorksFor(@"
+module Foo {
+
+  function Baz()
+    :(a: string)
+    ensures a == ""asdf""
+  {
+    ""asdf""
+  }
+
+  lemma Bar(t: string)
+    requires t == Baz()
+    ensures t == ""asdf""
+    {}
+}
+");
+    }
+    
+    [Fact]
   public void GitIssue3912FormatterCollectionArrow() {
     FormatterWorksFor(@"
 const i :=