---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MCBinarySearch.tla
---
---------------------------- MODULE MCBinarySearch -----------------------------
EXTENDS BinarySearch
CONSTANT MaxSeqLen
ASSUME MaxSeqLen \in Nat
LimitedSeq(S) == UNION {[1..n -> S]: n \in 1..MaxSeqLen}
================================================================================