From 29f437f859e3c7fad5a48fdce1fddc106991e586 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 28 Jul 2024 13:58:20 -0700 Subject: [PATCH] feat: Export GoalState.create --- Pantograph/Goal.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b44e8d3..6dbe525 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -33,6 +33,7 @@ structure GoalState where -- WARNING: If using `state with` outside of `calc`, this must be set to `.none` calcPrevRhs?: Option Expr := .none +@[export pantograph_goal_state_create_m] protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context. -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070