From 7a039e1f9e7424ea7d5c4abdabe20617bdc074cb Mon Sep 17 00:00:00 2001 From: adomani Date: Sat, 18 May 2024 17:39:49 +0200 Subject: [PATCH] use mathlib --- scripts/count_decls.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/count_decls.lean b/scripts/count_decls.lean index 5bc3fd93dc590..6c2f89bcaa566 100644 --- a/scripts/count_decls.lean +++ b/scripts/count_decls.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Kyle Miller. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kyle Miller, Damiano Testa -/ -import Mathlib.Data.Nat.Defs +import Mathlib --.Data.Nat.Defs /-! # `count_decls` -- a tally of declarations in `Mathlib` @@ -80,6 +80,6 @@ elab "count_decls" : command => do logInfo m!"{s.types.toArray}" -- logInfo s!"Theorems {s.thms}\nData {s.data}\nPredicates {s.preds}\nTypes {s.types}" -count_decls +--count_decls end PeriodicReports