feat: Do not explicitly show delay assigned mvar

This commit is contained in:
Leni Aniva 2024-05-06 22:39:17 -07:00
parent aa106f7591
commit 69ec70ffbe
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 7 additions and 4 deletions

View File

@ -102,7 +102,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
| .fvar fvarId =>
let name := ofName fvarId.name
pure s!"(:fv {name})"
| .mvar mvarId =>
| .mvar mvarId => do
if ← mvarId.isDelayedAssigned then
pure s!"(:mv)"
else
let name := ofName mvarId.name
pure s!"(:mv {name})"
| .sort level =>

View File

@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do
let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-- This is due to delayed assignment
addTest $ LSpec.test "(2 parent)" (state2parent ==
"((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
"((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state