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 :=