From 3b415e8dc12485f7b2b9fa6f54329f6ad598d48f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 23 Jul 2024 05:16:46 -0700 Subject: [PATCH] chore: Rename exports --- Pantograph/Expr.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 63331af..8ef0aa6 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -98,7 +98,7 @@ Convert an expression to an equiavlent form with 2. No aux lemmas 3. No assigned mvars -/ -@[export pantograph_instantiate_all_meta_m] +@[export pantograph_instantiate_all_m] def instantiateAll (e: Expr): MetaM Expr := do let e ← instantiateDelayedMVars e let e ← unfoldAuxLemmas e @@ -111,7 +111,7 @@ structure DelayedMVarInvocation where tail: Array Expr -- The pending mvar of any delayed assigned mvar must not be assigned in any way. -@[export pantograph_to_delayed_mvar_invocation_meta_m] +@[export pantograph_to_delayed_mvar_invocation_m] def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do let .mvar mvarId := e.getAppFn | return .none let .some decl ← getDelayedMVarAssignment? mvarId | return .none