From 23c53dc4dce354bcb2094c9d591fe1a8dec86481 Mon Sep 17 00:00:00 2001 From: Askar Safin Date: Thu, 23 Apr 2026 16:16:02 +0300 Subject: [PATCH] Update Defs.lean: correct description of `opaque` --- Manual/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/Defs.lean b/Manual/Defs.lean index d6b99f484..82e787b63 100644 --- a/Manual/Defs.lean +++ b/Manual/Defs.lean @@ -559,7 +559,7 @@ The {attr}`implemented_by` attribute can be used to instruct the compiler to emi :::syntax Lean.Parser.Command.declaration (alias := Lean.Parser.Command.opaque) (title := "Opaque Constants") Opaque definitions with right-hand sides are elaborated like other definitions. -This demonstrates that the type is inhabited; the inhabitant plays no further role. +This demonstrates that the type is inhabited; the inhabitant plays no further role in logic (but used in compiled code). ```grammar $_:declModifiers opaque $_ $_ := $_