MiniAgda-0.2025.7.23: test/fail/MixedMeasureLength.err
--- opening "MixedMeasureLength.ma" --- --- scope checking --- scope check error: in a mutual function block, either all functions must be without measure or have a measure of the same length
--- opening "MixedMeasureLength.ma" --- --- scope checking --- scope check error: in a mutual function block, either all functions must be without measure or have a measure of the same length