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