From 60f79f5f02f2debf0e121f20d8c409e148d74db6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 14 Apr 2025 23:26:14 -0700 Subject: [PATCH] doc: Fix typo --- Pantograph/Delate.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index a745854..a021b72 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr := self e := instantiateDelayedMVars e /-- -Convert an expression to an equiavlent form with +Convert an expression to an equivalent form with 1. No nested delayed assigned mvars 2. No aux lemmas or matchers 3. No assigned mvars