diff --git a/tests/compiler/foreign/Main/S.lean b/tests/compiler/foreign/Main/S.lean index a5ff00cdcb..3af72fa8e4 100644 --- a/tests/compiler/foreign/Main/S.lean +++ b/tests/compiler/foreign/Main/S.lean @@ -1,4 +1,4 @@ -constant SPointed : PointedType +constant SPointed : NonemptyType def S : Type := SPointed.type instance : Nonempty S := SPointed.property