From 70435dfb5ffb994d2eac99ae5ad4fa715835db53 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 7 Nov 2024 10:21:32 +0100 Subject: [PATCH] refactor: name the default SizeOf instance (#5981) This PR names the default SizeOf instance `instSizeOfDefault` I regularly have to debug termination checking failures where I end up hovering over some termination measure, and seeing `instSizeOfDefault` is more likely to tell me that the default instance is used than `instSizeOf`. --- src/Init/SizeOf.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean index 209967f59d..8be04fd32b 100644 --- a/src/Init/SizeOf.lean +++ b/src/Init/SizeOf.lean @@ -41,7 +41,11 @@ for every element of `α`. protected def default.sizeOf (α : Sort u) : α → Nat | _ => 0 -instance (priority := low) (α : Sort u) : SizeOf α where +/-- +Every type `α` has a low priority default `SizeOf` instance that just returns `0` +for every element of `α`. +-/ +instance (priority := low) instSizeOfDefault (α : Sort u) : SizeOf α where sizeOf := default.sizeOf α @[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl