From c40aed16287cd8ed6ad677648b523d6aa795f2e5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 16 Nov 2019 12:28:52 -0800 Subject: [PATCH] chore: typo --- library/Init/Lean/Expr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index cc5cb38d0d..ab385865d2 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.lean @@ -158,7 +158,7 @@ inductive Expr | lit : Literal → Data → Expr -- literals | mdata : MData → Expr → Data → Expr -- metadata | proj : Name → Nat → Expr → Data → Expr -- projection --- IMPORTANT: the following constructor will be delete +-- IMPORTANT: the following constructor will be deleted | localE : Name → Name → Expr → Data → Expr -- Lean2 legacy. TODO: delete namespace Expr