Add test for issue #4269

dafny-lang · Jul 10, 2023 · b5dd9dd · b5dd9dd
1 parent f4b7ccd
commit b5dd9dd
Showing 1 changed file with 20 additions and 0 deletions.
diff --git 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 :=