Mark in the environment extension that the given declaration has been declared by the user as noncomputable
.
Equations
Instances For
@[export lean_is_noncomputable]
Return true iff the user has declared the given declaration as noncomputable
.
Mark in the environment extension that the given declaration has been declared by the user as noncomputable
.
Return true iff the user has declared the given declaration as noncomputable
.