Run formatter

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -451,10 +451,10 @@ state properties of the otherwise uninterpreted or abstract type.
 ".TrimStart(), range =>
     range.Prev.val == "," ? [
         OneAction("remove comma", range.Prev, ""),
-        OneAction("insert '=='", range, "==" + range.PrintOriginal()),
-        OneAction("insert '0'", range, "0" + range.PrintOriginal()),
-        OneAction("insert '00'", range, "00" + range.PrintOriginal()),
-        OneAction("insert '!new'", range, "!new" + range.PrintOriginal())
+      OneAction("insert '=='", range, "==" + range.PrintOriginal()),
+      OneAction("insert '0'", range, "0" + range.PrintOriginal()),
+      OneAction("insert '00'", range, "00" + range.PrintOriginal()),
+      OneAction("insert '!new'", range, "!new" + range.PrintOriginal())
       ]
       : [
         OneAction("insert '=='", range, "==" + range.PrintOriginal()),

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -1109,7 +1109,7 @@ internal void PrintFormals(List<Formal> ff, ICallable/*?*/ context, string name
         wr.Write("[");
         PrintFormal(ff[0], false);
         wr.Write("]");
-        ff = [..ff.Skip(1)];
+        ff = [.. ff.Skip(1)];
       }
       wr.Write("(");
       string sep = "";

Source/DafnyCore/AST/TypeDeclarations/ArrayClassDecl.cs

@@ -10,7 +10,7 @@ public class ArrayClassDecl : ClassDecl {
   public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs)
     : base(SourceOrigin.NoToken, new Name(SystemModuleManager.ArrayClassName(dims)), module,
       [
-        ..new TypeParameter[]
+        .. new TypeParameter[]
           { new TypeParameter(SourceOrigin.NoToken, new Name("arg"), TypeParameter.TPVarianceSyntax.NonVariant_Strict) }
       ],
       [], attrs, false, null) {

Source/DafnyCore/AST/Types/Types.cs

@@ -493,7 +493,7 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris
             // This requires more recursion and bookkeeping than we care to try out
             return AutoInitInfo.MaybeEmpty;
           }
-          coDatatypesBeingVisited = [..coDatatypesBeingVisited];
+          coDatatypesBeingVisited = [.. coDatatypesBeingVisited];
         } else {
           coDatatypesBeingVisited = [];
         }

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -60,7 +60,7 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
     }
 
     private readonly Dictionary<ModuleDefinition, Import> ModuleImports = new();
-    private readonly List<Import> ImportsNotFromDafnyModules = [..StandardImports];
+    private readonly List<Import> ImportsNotFromDafnyModules = [.. StandardImports];
     private string ModuleName;
     private ModuleDefinition CurrentModule;
     private ConcreteSyntaxTree RootImportWriter;

Source/DafnyCore/DafnyOptions.cs

@@ -443,7 +443,7 @@ public DafnyOptions(DafnyOptions src, bool useNullWriters = false) : this(
       src.Input, src.OutputWriter, src.ErrorWriter) {
       src.CopyTo(this, useNullWriters);
       CliRootSourceUris = new List<Uri>(src.CliRootSourceUris);
-      ProverOptions = [..src.ProverOptions];
+      ProverOptions = [.. src.ProverOptions];
       Options = new Options(
         src.Options.OptionArguments.ToDictionary(kv => kv.Key, kv => kv.Value),
         src.Options.Arguments.ToDictionary(kv => kv.Key, kv => kv.Value));

Source/DafnyCore/Generic/Util.cs

@@ -172,7 +172,7 @@ public static List<A> Snoc<A>(List<A> xs, A x) {
     }
 
     public static List<A> Concat<A>(List<A> xs, List<A> ys) {
-      List<A> cpy = [..xs];
+      List<A> cpy = [.. xs];
       cpy.AddRange(ys);
       return cpy;
     }

Source/DafnyCore/Pipeline/Compilation.cs

@@ -520,7 +520,7 @@ public void CancelPendingUpdates() {
     }
     // TODO: end position doesn't take into account trailing trivia: https://github.com/dafny-lang/dafny/issues/3415
     return new TextEditContainer([
-      new() {NewText = result, Range = new Range(new Position(0,0), lastToken.GetLspPosition())}
+      new() { NewText = result, Range = new Range(new Position(0, 0), lastToken.GetLspPosition()) }
     ]);
 
   }

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -1873,7 +1873,7 @@ public void PartiallySolveTypeConstraints(bool allowDecisions) {
                 ProcessOneSubtypingConstraintAndItsSubs(c, processed, fullStrength, ref anyNewConstraints);
               }
 
-              allTypeConstraints = [..AllTypeConstraints];  // copy the list
+              allTypeConstraints = [.. AllTypeConstraints];  // copy the list
               foreach (var c in allTypeConstraints) {
                 var super = c.Super.NormalizeExpand() as TypeProxy;
                 if (AssignKnownEnd(super, true, fullStrength)) {

Source/DafnyCore/Rewriters/RefinementTransformer.cs

@@ -418,9 +418,9 @@ public bool CheckIsRefinement(ModuleDecl derived, AbstractModuleDecl original) {
         if (derivedPointer == original.OriginalSignature.ModuleDef) {
           HashSet<string> exports;
           if (derived is AliasModuleDecl) {
-            exports = [..((AliasModuleDecl)derived).Exports.ConvertAll(t => t.val)];
+            exports = [.. ((AliasModuleDecl)derived).Exports.ConvertAll(t => t.val)];
           } else if (derived is AbstractModuleDecl) {
-            exports = [..((AbstractModuleDecl)derived).Exports.ConvertAll(t => t.val)];
+            exports = [.. ((AbstractModuleDecl)derived).Exports.ConvertAll(t => t.val)];
           } else {
             Error(ErrorId.ref_base_module_must_be_abstract_or_alias, derived, "a module ({0}) can only be refined by an alias module or a module facade", original.Name);
             return false;

Source/DafnyCore/Triggers/ExprSubstituter.cs

@@ -49,7 +49,7 @@ public override Expression Substitute(Expression expr) {
           newBounds = [];
         } else if (newBounds == e.Bounds) {
           // create a new list with the same elements, since the .Add operations below would otherwise add elements to the original e.Bounds
-          newBounds = [..newBounds];
+          newBounds = [.. newBounds];
         }
 
         // conjoin all the new equalities to the range of the quantifier

Source/DafnyCore/Triggers/TriggerAnnotation.cs

@@ -16,8 +16,8 @@ internal TriggerAnnotation(bool isTriggerKiller,
     IEnumerable<TriggerTerm> privateTerms = null) {
     this.IsTriggerKiller = isTriggerKiller;
     this.Variables = new HashSet<IVariable>(variables);
-    this.PrivateTerms = [..privateTerms ?? []];
-    this.ExportedTerms = [..allTerms == null ? [] : allTerms.Except(this.PrivateTerms)];
+    this.PrivateTerms = [.. privateTerms ?? []];
+    this.ExportedTerms = [.. allTerms == null ? [] : allTerms.Except(this.PrivateTerms)];
   }
 
   public override string ToString() {

Source/DafnyCore/Triggers/TriggerTermSet.cs

@@ -67,7 +67,7 @@ private static TriggerTermSet Empty() {
   /// </summary>
   private TriggerTermSet CopyWithAdd(TriggerTerm term, IEnumerable<BoundVar> relevantVariables) {
     var copy = new TriggerTermSet();
-    copy.Terms = [..Terms];
+    copy.Terms = [.. Terms];
     copy.variables = new HashSet<BoundVar>(variables);
     copy.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>(termOwningAUniqueVar);
     copy.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>(uniqueVarsOwnedByATerm);

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1962,7 +1962,7 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
       private static readonly Dictionary<string, string> NullaryAttributesToTranslate;
 
       private static readonly HashSet<string> NullaryAttributesToCopy = [
-        ..new[] {
+        .. new[] {
           "focus",
           "isolate",
           "ignore",
@@ -1977,13 +1977,13 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
       ];
 
       private static readonly HashSet<string> BooleanAttributesToCopy = [
-        ..new[] {
+        .. new[] {
           "verify"
         }
       ];
 
       private static readonly HashSet<string> IntegerAttributesToCopy = [
-        ..new[] {
+        .. new[] {
           "subsumption",
           "testInline",
           "timeLimit",
@@ -1995,7 +1995,7 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
       ];
 
       private static readonly HashSet<string> StringAttributesToCopy = [
-        ..new[] {
+        .. new[] {
           "captureState",
           "isolate",
           "error"

Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs

@@ -317,7 +317,7 @@ public LetSuchThatExprInfo(IOrigin tok, int uniqueLetId,
         UsesHeap = usesHeap;
         UsesOldHeap = usesOldHeap;
         // we convert the set of heap-at variables to a list here, once and for all; the order itself is not material, what matters is that we always use the same order
-        UsesHeapAt = [..usesHeapAt];
+        UsesHeapAt = [.. usesHeapAt];
         ThisType = thisType;
       }
 

Source/DafnyCore/Verifier/ProofObligationDescription.cs

@@ -1541,8 +1541,8 @@ public override Expression GetAssertedExpr(DafnyOptions options) {
         : new UnaryOpExpr(sequence.Origin, UnaryOpExpr.Opcode.Cardinality, sequence);
       return new ChainingExpression(sequence.Origin, [
           new LiteralExpr(sequence.Origin, 0),
-          index,
-          bound
+        index,
+        bound
         ], [
           BinaryExpr.Opcode.Le,
           upperExcluded ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le

Source/DafnyDriver/Commands/GenerateTestsCommand.cs

@@ -137,7 +137,8 @@ internal static void PostProcess(DafnyOptions dafnyOptions, TestGenerationOption
     "Print the Boogie code used during test generation.") {
     ArgumentHelpName = "filename"
   };
-  public static readonly Option<string> ExpectedCoverageReport = new(["--expected-coverage-report", "--coverage-report"
+  public static readonly Option<string> ExpectedCoverageReport = new(["--expected-coverage-report",
+    "--coverage-report"
     ],
     "Emit expected test coverage report to a given directory.") {
     ArgumentHelpName = "directory"

Source/DafnyLanguageServer/MarkupTestFile.cs

@@ -168,7 +168,7 @@ public static void GetPositionsAndRanges(string input, out string output, out IL
       GetIndexAndSpans(input, out output, out var positionIndices, out var spans);
       var buffer = new TextBuffer(output);
       positions = positionIndices.Select(index => buffer.FromIndex(index)).ToList();
-      ranges = [..spans.Select(span => new Range(buffer.FromIndex(span.Span.Start), buffer.FromIndex(span.Span.End)))];
+      ranges = [.. spans.Select(span => new Range(buffer.FromIndex(span.Span.Start), buffer.FromIndex(span.Span.End)))];
     }
 
     public static void GetPositionAndRanges(string input, out string output, out Position cursorPosition, out ImmutableArray<Range> ranges) {