From d57612ec71e9f0416d1e42dc01f030522abbc901 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 15 Feb 2024 14:47:09 -0800
Subject: [PATCH] test: Delayed metavariable assignment

---
 Test/Proofs.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 07e4cea..85ba66d 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -232,6 +232,11 @@ def proof_or_comm: TestM Unit := do
   addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
+  let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
+  -- This is due to delayed assignment
+  addTest $ LSpec.test "(2 parent)" (state2parent ==
+    "((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+
   let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do