We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 7aaaa0e commit 1f7e555Copy full SHA for 1f7e555
src/Init/SizeOf.lean
@@ -45,7 +45,7 @@ protected def default.sizeOf (α : Sort u) : α → Nat
45
Every type `α` has a low priority default `SizeOf` instance that just returns `0`
46
for every element of `α`.
47
-/
48
-instance (priority := low) (α : Sort u) instSizeOfDefault : SizeOf α where
+instance (priority := low) instSizeOfDefault (α : Sort u) : SizeOf α where
49
sizeOf := default.sizeOf α
50
51
@[simp] theorem sizeOf_default (n : α) : sizeOf n = 0 := rfl
0 commit comments