Refactor all operator descriptions/comments into what SANY considers proper pre-comments.

[lemmy]

Old parse tree

| | N_OperatorDefinition	*ReplaceAllSubSeqs	  #heirs: 3	  kind:   389
| | | N_IdentLHS	  #heirs: 8	  kind:   366
| | | | ReplaceAllSubSeqs	  #heirs: 0	  kind:   292
| | | | (	  #heirs: 0	  kind:   94
| | | | N_IdentDecl	  #heirs: 1	  kind:   363
| | | | | r	  #heirs: 0	  kind:   292
| | | | ,	  #heirs: 0	  kind:   88
| | | | N_IdentDecl	  #heirs: 1	  kind:   363
| | | | | s	  #heirs: 0	  kind:   292
| | | | ,	  #heirs: 0	  kind:   88
| | | | N_IdentDecl	  #heirs: 1	  kind:   363
| | | | | t	  #heirs: 0	  kind:   292
| | | | )	  #heirs: 0	  kind:   95
| | | ==	  #heirs: 0	  kind:   93
| | | N_Case	  #heirs: 10	  kind:   336
| | | | CASE	  #heirs: 0	  kind:   42
 preComment: 0 (**************************************************************************)
             1 (* The sequence  t  with all subsequences  s  replaced by the sequence  r *)
             2 (* Overlapping replacements are disambiguated by choosing the occurrence  *)
             3 (* closer to the beginning of the sequence.                               *)
             4 (*                                                                        *)
             5 (* Examples:                                                              *)
             6 (*                                                                        *)
             7 (*  ReplaceAllSubSeqs(<<>>,<<>>,<<>>) = <<>>                              *)
             8 (*  ReplaceAllSubSeqs(<<4>>,<<>>,<<>>) = <<4>>                            *)
             9 (*  ReplaceAllSubSeqs(<<2>>,<<3>>,<<1,3>>) = <<1,2>>                      *)
             10 (*  ReplaceAllSubSeqs(<<2,2>>,<<1,1>>,<<1,1,1>>) = <<2,2,1>>              *)
             11 (**************************************************************************)

New parse tree

| | N_OperatorDefinition	*ReplaceAllSubSeqs	  #heirs: 3	  kind:   389
| | | N_IdentLHS	  #heirs: 8	  kind:   366
| | | | ReplaceAllSubSeqs	  #heirs: 0	  kind:   292
 preComment: 0 (**************************************************************************)
             1 (* The sequence  t  with all subsequences  s  replaced by the sequence  r *)
             2 (* Overlapping replacements are disambiguated by choosing the occurrence  *)
             3 (* closer to the beginning of the sequence.                               *)
             4 (*                                                                        *)
             5 (* Examples:                                                              *)
             6 (*                                                                        *)
             7 (*  ReplaceAllSubSeqs(<<>>,<<>>,<<>>) = <<>>                              *)
             8 (*  ReplaceAllSubSeqs(<<4>>,<<>>,<<>>) = <<4>>                            *)
             9 (*  ReplaceAllSubSeqs(<<2>>,<<3>>,<<1,3>>) = <<1,2>>                      *)
             10 (*  ReplaceAllSubSeqs(<<2,2>>,<<1,1>>,<<1,1,1>>) = <<2,2,1>>              *)
             11 (**************************************************************************)

[Refactor]

[Copilot]

Pull Request Overview

This pull request refactors the operator descriptions and comments across multiple modules to conform with SANY’s proper pre-comment style. Key changes include replacing verbose comment blocks with succinct pre-comments or stubs, updating operator definitions in modules like SequencesExt.tla, Json.tla, IOUtils.tla, and others, and standardizing placeholder implementations where full logic is yet to be provided.

Reviewed Changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
modules/Statistics.tla	Updated ChiSquare operator to a stub with a TODO note.
modules/SequencesExt.tla	Refactored several sequence operators; note potential incomplete CASE statement in ReplaceAllSubSeqs.
modules/SVG.tla	Updated SVG element functions; NodeOfRingNetwork now returns a stub value.
modules/Json.tla	Streamlined JSON conversion operators to rely on simplified checks.
modules/IOUtils.tla	Converted serialization and external command functions to stub implementations.
modules/Functions.tla	Adjusted fold functions using MapThenFoldSet.
modules/FiniteSetsExt.tla	Refactored set operations including FoldSet and Quantify.
modules/Bitwise.tla	Updated infix bitwise operator definitions with minor refactoring.
modules/BagsExt.tla	Simplified bag operations and fold functions using MapThenFoldBag.

[lemmy]

Related: tlaplus/vscode-tlaplus#378