From 71327d2d55f541c532d74c9e4563f47a23b2f458 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 27 Aug 2023 22:50:18 -0700 Subject: [PATCH] Separate max and imax in sort level --- Pantograph/Serial.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 6dd9a9f..924c77b 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -83,16 +83,20 @@ def serialize_sort_level_ast (level: Level): String := let u_str := match u with | .zero => "0" | .succ _ => panic! "getLevelOffset should not return .succ" - | .max v w | .imax v w => + | .max v w => let v := serialize_sort_level_ast v let w := serialize_sort_level_ast w - s!"(max {v} {w})" + s!"(:max {v} {w})" + | .imax v w => + let v := serialize_sort_level_ast v + let w := serialize_sort_level_ast w + s!"(:imax {v} {w})" | .param name => let name := name_to_ast name s!"{name}" | .mvar id => let name := name_to_ast id.name - s!"(:mvar {name})" + s!"(:mv {name})" match k, u with | 0, _ => u_str | _, .zero => s!"{k}"