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 88ddb39 commit 3729103Copy full SHA for 3729103
src/Lean/Compiler/NoncomputableAttr.lean
@@ -15,7 +15,7 @@ def addNoncomputable (env : Environment) (declName : Name) : Environment :=
15
noncomputableExt.tag env declName
16
17
/--
18
-Return true iff the user has declared the given declaration as `noncomputable`.
+Returns `true` when the given declaration is tagged `noncomputable`.
19
-/
20
@[export lean_is_noncomputable]
21
def isNoncomputable (env : Environment) (declName : Name) : Bool :=
0 commit comments