From 87f0dabbb5c160730899e1daabe3b247079c2bdc Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 3 Feb 2025 11:57:41 +0000 Subject: [PATCH] Update stats.lean --- scripts/stats.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/stats.lean b/scripts/stats.lean index d8d1c9b..4227fd0 100644 --- a/scripts/stats.lean +++ b/scripts/stats.lean @@ -16,7 +16,6 @@ This file concerns with statistics of HepLean. open Lean System Meta HepLean - def getStats : MetaM String := do let noDefsVal ← noDefs let noLemmasVal ← noLemmas